Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 156 insertions, 188 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index ab863eb1f..bde3d9a92 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -10,7 +10,7 @@ Open Local Scope NatIntScope.
 Notation Z := NZ (only parsing).
 Notation E := NZE (only parsing).
 
-Parameter Inline Zopp : Z -> Z.
+Parameter Zopp : Z -> Z.
 
 Add Morphism Zopp with signature E ==> E as Zopp_wd.
 
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 295f5355a..e0ef2f15d 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -23,6 +23,9 @@ Proof NZlt_le_incl.
 Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem Zle_refl : forall n : Z, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index bab1bb4a0..6a13aa3db 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -30,14 +30,32 @@ Proof NZplus_lt_le_mono.
 Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
 Proof NZplus_le_lt_mono.
 
+Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZplus_pos_pos.
+
+Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
+Proof NZplus_pos_nonneg.
+
+Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
+Proof NZplus_nonneg_pos.
+
+Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof NZplus_nonneg_nonneg.
+
+Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m.
+Proof NZlt_plus_pos_l.
+
+Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n.
+Proof NZlt_plus_pos_r.
+
 Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
 Proof NZle_lt_plus_lt.
 
 Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
 Proof NZlt_le_plus_lt.
 
-Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_lt.
+Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_le.
 
 Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
 Proof NZplus_lt_cases.
@@ -57,89 +75,6 @@ Proof NZplus_nonpos_cases.
 Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof NZplus_nonneg_cases.
 
-(** Multiplication and order *)
-
-Theorem Ztimes_lt_pred :
-  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
-
-Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
-
-Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
-
-Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
-Proof NZtimes_lt_mono_neg_l.
-
-Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
-Proof NZtimes_lt_mono_neg_r.
-
-Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
-Proof NZtimes_le_mono_nonneg_l.
-
-Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
-Proof NZtimes_le_mono_nonpos_l.
-
-Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
-Proof NZtimes_le_mono_nonneg_r.
-
-Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
-Proof NZtimes_le_mono_nonpos_r.
-
-Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
-
-Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
-
-Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
-
-Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
-Proof NZtimes_le_mono_neg_l.
-
-Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
-Proof NZtimes_le_mono_neg_r.
-
-Theorem Ztimes_lt_mono :
-  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
-Proof NZtimes_lt_mono.
-
-Theorem Ztimes_le_mono :
-  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
-Proof NZtimes_le_mono.
-
-Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZtimes_pos_pos.
-
-Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
-Proof NZtimes_nonneg_nonneg.
-
-Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
-Proof NZtimes_neg_neg.
-
-Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
-Proof NZtimes_nonpos_nonpos.
-
-Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
-Proof NZtimes_pos_neg.
-
-Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
-Proof NZtimes_nonneg_nonpos.
-
-Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
-Proof NZtimes_neg_pos.
-
-Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
-Proof NZtimes_nonpos_nonneg.
-
-Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
-Proof NZtimes_eq_0.
-
-Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZtimes_neq_0.
-
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (** Minus and order *)
@@ -252,7 +187,7 @@ Qed.
 
 Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
-intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n));
+intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n));
 [now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index d63dc0d8c..438142095 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -94,6 +94,9 @@ Theorem Ztimes_neg :
   forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
 Proof NZtimes_neg.
 
+Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (* None? *)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index cb8ac3b5b..0a52d214a 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -132,7 +132,14 @@ Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp := Zopp.
+Definition Zopp (x : Z) :=
+match x with
+| Z0 => Z0
+| Zpos x => Zneg x
+| Zneg x => Zpos x
+end.
+
+Notation "- x" := (Zopp x) : Z_scope.
 
 Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 5c8b5890d..9a012b26c 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,48 +1,82 @@
 Require Import NMinus. (* The most complete file for natural numbers *)
-Require Import ZTimesOrder. (* The most complete file for integers *)
+Require Export ZTimesOrder. (* The most complete file for integers *)
 
 Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
 Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
-Notation Local N := NZ. (* To remember N without having to use a long qualifying name *)
-Notation Local NE := NZE (only parsing).
-Notation Local plus_wd := NZplus_wd (only parsing).
+
+(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
+the properties functor. Since we don't want Zplus_comm to refer to unfolded
+definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
+we will provide an extra layer of definitions. *)
+
 Open Local Scope NatIntScope.
+Definition Z := (N * N)%type.
+Definition Z0 : Z := (0, 0).
+Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
+Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
 
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
+(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It
+could be possible to consider as canonical only pairs where one of the
+elements is 0, and make all operations convert canonical values into other
+canonical values. In that case, we could get rid of setoids as well as
+arrive at integers as signed natural numbers. *)
+
+Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
+Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
 
-Definition NZ : Set := (NZ * NZ)%type.
-Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
-Notation Z := NZ (only parsing).
-Notation E := NZE (only parsing).
-Definition NZ0 := (0, 0).
-Definition NZsucc (n : Z) := (S (fst n), snd n).
-Definition NZpred (n : Z) := (fst n, S (snd n)).
-(* We do not have P (S n) = n but only P (S n) == n. It could be possible
-to consider as canonical only pairs where one of the elements is 0, and
-make all operations convert canonical values into other canonical values.
-In that case, we could get rid of setoids as well as arrive at integers as
-signed natural numbers. *)
-Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
-Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
-Definition NZtimes (n m : Z) :=
+
+Definition Ztimes (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
+Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
+Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
 
-Theorem ZE_refl : reflexive Z E.
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
+Notation "0" := Z0 : IntScope.
+Notation "1" := (Zsucc Z0) : IntScope.
+Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x < y" := (Zlt x y) : IntScope.
+Notation "x <= y" := (Zle x y) : IntScope.
+Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+
+Notation Local N := NZ.
+(* To remember N without having to use a long qualifying name. since NZ will be redefined *)
+Notation Local NE := NZE (only parsing).
+Notation Local plus_wd := NZplus_wd (only parsing).
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ : Set := Z.
+Definition NZE := Zeq.
+Definition NZ0 := Z0.
+Definition NZsucc := Zsucc.
+Definition NZpred := Zpred.
+Definition NZplus := Zplus.
+Definition NZminus := Zminus.
+Definition NZtimes := Ztimes.
+
+Theorem ZE_refl : reflexive Z Zeq.
 Proof.
-unfold reflexive, E; reflexivity.
+unfold reflexive, Zeq. reflexivity.
 Qed.
 
-Theorem ZE_symm : symmetric Z E.
+Theorem ZE_symm : symmetric Z Zeq.
 Proof.
-unfold symmetric, E; now symmetry.
+unfold symmetric, Zeq; now symmetry.
 Qed.
 
-Theorem ZE_trans : transitive Z E.
+Theorem ZE_trans : transitive Z Zeq.
 Proof.
-unfold transitive, E. intros n m p H1 H2.
+unfold transitive, Zeq. intros n m p H1 H2.
 assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
 by now apply plus_wd.
 stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
@@ -50,46 +84,46 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> plus_cancel_r in H3.
 Qed.
 
-Theorem NZE_equiv : equiv Z E.
+Theorem NZE_equiv : equiv Z Zeq.
 Proof.
 unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
 Qed.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 NZE_equiv)
  symmetry proved by (proj2 (proj2 NZE_equiv))
  transitivity proved by (proj1 (proj2 NZE_equiv))
 as NZE_rel.
 
-Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd.
+Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
-intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
+intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZsucc with signature E ==> E as NZsucc_wd.
+Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
 Proof.
-unfold NZsucc, E; intros n m H; simpl.
+unfold NZsucc, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_l; now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature E ==> E as NZpred_wd.
+Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
 Proof.
-unfold NZpred, E; intros n m H; simpl.
+unfold NZpred, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd.
+Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd.
 Proof.
-unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
 by now apply plus_wd.
 stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
 
-Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd.
+Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd.
 Proof.
-unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
 assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
 by now apply plus_wd.
@@ -97,9 +131,9 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd.
+Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd.
 Proof.
-unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
 apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
@@ -117,39 +151,20 @@ apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
 ring.
 Qed.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with NZ.
-Open Local Scope IntScope.
-Notation "x == y"  := (NZE x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
-Notation "1" := (S 0) : IntScope.
-Notation "x + y" := (NZplus x y) : IntScope.
-Notation "x - y" := (NZminus x y) : IntScope.
-Notation "x * y" := (NZtimes x y) : IntScope.
-
-Theorem NZpred_succ : forall n : Z, P (S n) == n.
-Proof.
-unfold NZpred, NZsucc, E; intro n; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
-Qed.
-
 Section Induction.
 Open Scope NatIntScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd E A.
+Hypothesis A_wd : predicate_wd Zeq A.
 
-Add Morphism A with signature E ==> iff as A_morph.
+Add Morphism A with signature Zeq ==> iff as A_morph.
 Proof.
 exact A_wd.
 Qed.
 
 Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
 Proof.
-intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *.
+intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
@@ -166,51 +181,56 @@ Qed.
 
 End Induction.
 
+(* Time to prove theorems in the language of Z *)
+
+Open Local Scope IntScope.
+
+Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
+Proof.
+unfold NZpred, NZsucc, Zeq; intro n; simpl.
+rewrite plus_succ_l; now rewrite plus_succ_r.
+Qed.
+
 Theorem NZplus_0_l : forall n : Z, 0 + n == n.
 Proof.
-intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l.
+intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
+Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
 Proof.
-intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l.
+intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l.
 Qed.
 
 Theorem NZminus_0_r : forall n : Z, n - 0 == n.
 Proof.
-intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r.
+intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r.
+intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r.
 Qed.
 
 Theorem NZtimes_0_r : forall n : Z, n * 0 == 0.
 Proof.
-intro n; unfold NZtimes, E; simpl.
+intro n; unfold NZtimes, Zeq; simpl.
 repeat rewrite times_0_r. now rewrite plus_assoc.
 Qed.
 
-Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n.
 Proof.
-intros n m; unfold NZtimes, NZsucc, E; simpl.
+intros n m; unfold NZtimes, NZsucc, Zeq; simpl.
 do 2 rewrite times_succ_r. ring.
 Qed.
 
 End NZAxiomsMod.
 
-Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
-Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
-
-Notation "x < y" := (NZlt x y) : IntScope.
-Notation "x <= y" := (NZle x y) : IntScope.
-Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
+Definition NZlt := Zlt.
+Definition NZle := Zle.
 
-Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
+Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
-unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
+unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
 stepr (snd m1 + fst m2) by apply plus_comm.
 apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
 stepl (snd m2 + fst n1) by apply plus_comm.
@@ -227,58 +247,58 @@ now stepl (fst m1 + snd m2) by apply plus_comm.
 stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
 Qed.
 
-Open Local Scope IntScope.
-
-Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
+Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
 Proof.
-unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl.
-do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2).
-fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2.
+unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
+do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
+fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2.
 now rewrite H1, H2.
 Qed.
 
+Open Local Scope IntScope.
+
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq.
+intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq.
 Qed.
 
 Theorem NZlt_irrefl : forall n : Z, ~ (n < n).
 Proof.
-intros n; unfold NZlt, E; simpl. apply lt_irrefl.
+intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl.
 Qed.
 
-Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m.
+Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le.
+intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le.
 Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp (n : Z) := (snd n, fst n).
+Definition Zopp (n : Z) : Z := (snd n, fst n).
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+Notation "- x" := (Zopp x) : IntScope.
 
-Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 Proof.
-unfold E; intros n m H; simpl. symmetry.
+unfold Zeq; intros n m H; simpl. symmetry.
 stepl (fst n + snd m) by apply plus_comm.
 now stepr (fst m + snd n) by apply plus_comm.
 Qed.
 
 Open Local Scope IntScope.
 
-Theorem Zsucc_pred : forall n : Z, S (P n) == n.
+Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
 Proof.
-intro n; unfold NZsucc, NZpred, E; simpl.
+intro n; unfold Zsucc, Zpred, Zeq; simpl.
 rewrite plus_succ_l; now rewrite plus_succ_r.
 Qed.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof.
-unfold Zopp, E; simpl. now rewrite plus_0_l.
+unfold Zopp, Zeq; simpl. now rewrite plus_0_l.
 Qed.
 
-Theorem Zopp_succ : forall n, - (S n) == P (- n).
+Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
 Proof.
 reflexivity.
 Qed.