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
].