Library Coq.ring.LegacyZArithRing




Require Export LegacyArithRing.
Require Export ZArith_base.
Require Import Eqdep_dec.
Require Import LegacyRing.


Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.

Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
Qed.

Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
 [ Zpos Zneg 0%Z xO xI 1%positive ].