Timings for Rings_Z.v

1. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./setoid_ring/Rings_Z.timing
2. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./setoid_ring/Rings_Z.timing

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export Cring.
Require Export Integral_domain.
Require Export Ncring_initial.

#[global]
Instance Zcri: (Cring (Rr:=Zr)).
red.
 exact Z.mul_comm.
 Defined.

Lemma Z_one_zero: 1%Z <> 0%Z.
Proof.
 discriminate.
 Qed.

#[global]
Instance Zdi : (Integral_domain (Rcr:=Zcri)).
 
constructor.
 
-
 exact Zmult_integral.
-
 exact Z_one_zero.
Defined.