Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

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

13 files changed, 97 insertions, 136 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index bde3d9a920..0e47356ada 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -1,20 +1,39 @@
-Require Export NumPrelude.
 Require Export NZAxioms.
 
 Set Implicit Arguments.
 
 Module Type ZAxiomsSig.
 Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
-Open Local Scope NatIntScope.
 
-Notation Z := NZ (only parsing).
-Notation E := NZE (only parsing).
+Delimit Scope IntScope with Int.
+Notation Z := NZ.
+Notation Zeq := NZeq.
+Notation Z0 := NZ0.
+Notation Z1 := (NZsucc NZ0).
+Notation S := NZsucc.
+Notation P := NZpred.
+Notation Zplus := NZplus.
+Notation Ztimes := NZtimes.
+Notation Zminus := NZminus.
+Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
+Notation "0" := NZ0 : IntScope.
+Notation "1" := (NZsucc NZ0) : IntScope.
+Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x - y" := (NZminus x y) : IntScope.
+Notation "x * y" := (NZtimes x y) : IntScope.
+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.
 
 Parameter Zopp : Z -> Z.
 
-Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : NatIntScope.
+Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+
+Open Local Scope IntScope.
 
 (* Integers are obtained by postulating that every number has a predecessor *)
 Axiom Zsucc_pred : forall n : Z, S (P n) == n.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9f5ff8bd37..dbe2aa4396 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,8 +1,9 @@
 Require Export ZAxioms.
 Require Import NZTimesOrder.
 
-Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Open Local Scope NatIntScope.
+Module ZBasePropFunct (Export ZAxiomsMod : ZAxiomsSig).
+
+Open Local Scope IntScope.
 
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
@@ -22,7 +23,7 @@ Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
 Theorem Zcentral_induction :
-forall A : Z -> Prop, predicate_wd E A ->
+forall A : Z -> Prop, predicate_wd Zeq A ->
   forall z : Z, A z ->
     (forall n : Z, A n <-> A (S n)) ->
       forall n : Z, A n.
diff --git a/theories/Numbers/Integer/Abstract/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v
deleted file mode 100644
index 843b48b936..0000000000
--- a/theories/Numbers/Integer/Abstract/ZDec.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
-
-
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 7ace860f38..3146b9c2c3 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -3,13 +3,13 @@ Require Export NumPrelude.
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
-Parameter Inline E : Z -> Z -> Prop.
+Parameter Inline Zeq : Z -> Z -> Prop.
 Parameter Inline e : Z -> Z -> bool.
 
-Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
-Axiom E_equiv : equiv Z E.
+Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom E_equiv : equiv Z Zeq.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 E_equiv)
  symmetry proved by (proj2 (proj2 E_equiv))
  transitivity proved by (proj1 (proj2 E_equiv))
@@ -17,15 +17,15 @@ as E_rel.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
-Notation "x == y" := (E x y) (at level 70) : IntScope.
-Notation "x # y" := (~ E x y) (at level 70) : IntScope.
+Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
+Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
 
 End ZDomainSignature.
 
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
+Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
 Proof.
 intros x x' Exx' y y' Eyy'.
 case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
@@ -49,7 +49,7 @@ Qed.
 
 Declare Left Step ZE_stepl.
 
-(* The right step lemma is just transitivity of E *)
+(* The right step lemma is just transitivity of Zeq *)
 Declare Right Step (proj1 (proj2 E_equiv)).
 
 End ZDomainProperties.
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index e0ef2f15d9..7eed9a8eeb 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -2,7 +2,7 @@ Require Export ZTimes.
 
 Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (* Axioms *)
 
@@ -140,21 +140,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
         forall n : Z, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -162,7 +162,7 @@ Theorem Zorder_induction :
 Proof NZorder_induction.
 
 Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
       (forall n : Z, n <= z -> A n -> A (P n)) ->
@@ -175,7 +175,7 @@ unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
 Qed.
 
 Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
@@ -183,7 +183,7 @@ Theorem Zright_induction' :
 Proof NZright_induction'.
 
 Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
@@ -193,7 +193,7 @@ Proof NZstrong_right_induction'.
 (** Elimintation principle for < *)
 
 Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall n : Z,
       A (S n) ->
       (forall m : Z, n < m -> A m -> A (S m)) ->
@@ -203,7 +203,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall n : Z,
       A n ->
       (forall m : Z, n <= m -> A m -> A (S m)) ->
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index c22b346b43..bae74feca2 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -2,7 +2,7 @@ Require Export ZBase.
 
 Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 Theorem Zplus_0_l : forall n : Z, 0 + n == n.
 Proof NZplus_0_l.
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 6a13aa3db6..49fd6f5588 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -2,7 +2,7 @@ Require Export ZOrder.
 
 Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (** Theorems that are true on both natural numbers and integers *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v
deleted file mode 100644
index 4814ab086b..0000000000
--- a/theories/Numbers/Integer/Abstract/ZPred.v
+++ /dev/null
@@ -1,54 +0,0 @@
-Axiom succ_pred : forall x : Z, S (P x) == x.
-Add Morphism P with signature E ==> E as pred_wd.
-
-Theorem pred_inj : forall x y, P x == P y -> x == y.
-Proof.
-intros x y H.
-setoid_replace x with (S (P x)); [| symmetry; apply succ_pred].
-setoid_replace y with (S (P y)); [| symmetry; apply succ_pred].
-now rewrite H.
-Qed.
-
-Theorem pred_succ : forall x, P (S x) == x.
-Proof.
-intro x.
-apply succ_inj.
-now rewrite succ_pred.
-Qed.
-
-(* The following tactics are intended for replacing a certain
-occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
-Unfortunately, this cannot be done by setoid_replace tactic for two
-reasons. First, it seems impossible to do rewriting when one side of
-the equation in question (succ_pred or pred_succ) is a variable, due to bug 1604.
-This does not work even when the predicate is an identifier (e.g.,
-when one tries to rewrite (A x) into (A (S (P x)))). Second, the
-setoid_rewrite tactic, like the ordinary rewrite tactic, does not
-allow specifying the exact occurrence of the term to be rewritten. Now
-while not in the setoid context, this occurrence can be specified
-using the pattern tactic, it does not work with setoids, since pattern
-creates a lambda abstractuion, and setoid_rewrite does not work with
-them. *)
-
-Ltac rewrite_succP t set_tac repl thm :=
-let x := fresh "x" in
-set_tac x t;
-setoid_replace x with (repl x); [| symmetry; apply thm];
-unfold x; clear x.
-
-Tactic Notation "rewrite_succ_pred" constr(t) :=
-rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred.
-
-Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) :=
-rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred.
-
-Tactic Notation "rewrite_pred_succ" constr(t) :=
-rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ.
-
-Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) :=
-rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ.
-
-(* One can add tactic notations for replacements in assumptions rather
-than in the goal. For the reason of many possible variants, the core
-of the tactic is factored out. *)
-
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index bc7321cbae..0290c237bb 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -3,7 +3,7 @@ Require Export ZPlus.
 
 Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
@@ -48,7 +48,7 @@ Proof NZtimes_neq_0.
 
 (** Z forms a ring *)
 
-Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZE.
+Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq.
 Proof.
 constructor.
 exact Zplus_0_l.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 4381420950..b1a0551f89 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -2,7 +2,7 @@ Require Export ZPlusOrder.
 
 Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (** Theorems that are true on both natural numbers and integers *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0a52d214a2..85596562e3 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -8,7 +8,7 @@ Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
 
 Definition NZ := Z.
-Definition NZE := (@eq Z).
+Definition NZeq := (@eq Z).
 Definition NZ0 := 0.
 Definition NZsucc := Zsucc'.
 Definition NZpred := Zpred'.
@@ -16,38 +16,38 @@ Definition NZplus := Zplus.
 Definition NZminus := Zminus.
 Definition NZtimes := Zmult.
 
-Theorem NZE_equiv : equiv Z NZE.
+Theorem NZE_equiv : equiv Z NZeq.
 Proof.
 exact (@eq_equiv Z).
 Qed.
 
-Add Relation Z NZE
+Add Relation Z NZeq
  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 NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
+Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
+Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
 Proof.
 congruence.
 Qed.
@@ -58,7 +58,7 @@ exact Zpred'_succ'.
 Qed.
 
 Theorem NZinduction :
-  forall A : Z -> Prop, predicate_wd NZE A ->
+  forall A : Z -> Prop, predicate_wd NZeq A ->
     A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n.
 Proof.
 intros A A_wd A0 AS n; apply Zind; clear n.
@@ -103,14 +103,14 @@ End NZAxiomsMod.
 Definition NZlt := Zlt.
 Definition NZle := Zle.
 
-Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
 Proof.
-unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
+unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
 Proof.
-unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
+unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
 Qed.
 
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m.
@@ -139,9 +139,7 @@ match x with
 | Zneg x => Zpos x
 end.
 
-Notation "- x" := (Zopp x) : Z_scope.
-
-Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd.
+Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd.
 Proof.
 congruence.
 Qed.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 9a012b26cf..38e8e097ad 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -49,14 +49,14 @@ 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 NE := NZeq (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 NZeq := Zeq.
 Definition NZ0 := Z0.
 Definition NZsucc := Zsucc.
 Definition NZpred := Zpred.
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index 7479868e9d..2d63a22faf 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -16,7 +16,7 @@ Notation Local wB := (base w_op.(znz_digits)).
 
 Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
 
-Definition NZE (n m : NZ) := [| n |] = [| m |].
+Definition NZeq (n m : NZ) := [| n |] = [| m |].
 Definition NZ0 := w_op.(znz_0).
 Definition NZsucc := w_op.(znz_succ).
 Definition NZpred := w_op.(znz_pred).
@@ -24,51 +24,51 @@ Definition NZplus := w_op.(znz_add).
 Definition NZminus := w_op.(znz_sub).
 Definition NZtimes := w_op.(znz_mul).
 
-Theorem NZE_equiv : equiv NZ NZE.
+Theorem NZE_equiv : equiv NZ NZeq.
 Proof.
-unfold equiv, reflexive, symmetric, transitive, NZE; repeat split; intros; auto.
+unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
 now transitivity [| y |].
 Qed.
 
-Add Relation NZ NZE
+Add Relation NZ NZeq
  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 NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
-unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
+unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
+Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
 Proof.
-unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
+unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
 Proof.
-unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
+unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
+Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
 Proof.
-unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
+unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
 Proof.
-unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
+unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
 now rewrite H1, H2.
 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 "x == y"  := (NZeq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
 Notation "'S'" := NZsucc : IntScope.
 Notation "'P'" := NZpred : IntScope.
@@ -110,14 +110,14 @@ Qed.
 
 Theorem NZpred_succ : forall n : NZ, P (S n) == n.
 Proof.
-intro n; unfold NZsucc, NZpred, NZE. rewrite w_spec.(spec_pred), w_spec.(spec_succ).
+intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ).
 rewrite <- NZpred_mod_wB.
 replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
 Qed.
 
 Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int.
 Proof.
-unfold NZE, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct.
+unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct.
 symmetry; apply w_spec.(spec_0).
 exact w_spec. split; [auto with zarith |apply gt_wB_0].
 Qed.
@@ -125,11 +125,11 @@ Qed.
 Section Induction.
 
 Variable A : NZ -> Prop.
-Hypothesis A_wd : predicate_wd NZE A.
+Hypothesis A_wd : predicate_wd NZeq A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
 
-Add Morphism A with signature NZE ==> iff as A_morph.
+Add Morphism A with signature NZeq ==> iff as A_morph.
 Proof A_wd.
 
 Let B (n : Z) := A (Z_to_NZ n).
@@ -143,8 +143,8 @@ Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
 Proof.
 intros n H1 H2 H3.
 unfold B in *. apply -> AS in H3.
-setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZE. assumption.
-unfold NZE. rewrite w_spec.(spec_succ).
+setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption.
+unfold NZeq. rewrite w_spec.(spec_succ).
 unfold NZ_to_Z, Z_to_NZ.
 do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
 symmetry; apply Zmod_def_small; auto with zarith.
@@ -159,9 +159,9 @@ Qed.
 
 Theorem NZinduction : forall n : NZ, A n.
 Proof.
-intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZE.
+intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq.
 apply B_holds. apply w_spec.(spec_to_Z).
-unfold NZE, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
+unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
 reflexivity.
 exact w_spec.
 apply w_spec.(spec_to_Z).
@@ -171,13 +171,13 @@ End Induction.
 
 Theorem NZplus_0_l : forall n : NZ, 0 + n == n.
 Proof.
-intro n; unfold NZplus, NZ0, NZE. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
+intro n; unfold NZplus, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
 rewrite Zplus_0_l. rewrite Zmod_def_small; [reflexivity | apply w_spec.(spec_to_Z)].
 Qed.
 
 Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 Proof.
-intros n m; unfold NZplus, NZsucc, NZE. rewrite w_spec.(spec_add).
+intros n m; unfold NZplus, NZsucc, NZeq. rewrite w_spec.(spec_add).
 do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add).
 rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
 rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l; [ |apply gt_wB_0].
@@ -186,13 +186,13 @@ Qed.
 
 Theorem NZminus_0_r : forall n : NZ, n - 0 == n.
 Proof.
-intro n; unfold NZminus, NZ0, NZE. rewrite w_spec.(spec_sub).
+intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub).
 rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod.
 Qed.
 
 Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
 Proof.
-intros n m; unfold NZminus, NZsucc, NZpred, NZE.
+intros n m; unfold NZminus, NZsucc, NZpred, NZeq.
 rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub).
 rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r; [ | apply gt_wB_0].
 rewrite Zminus_mod_idemp_l; [ | apply gt_wB_0].
@@ -201,13 +201,13 @@ Qed.
 
 Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0.
 Proof.
-intro n; unfold NZtimes, NZ0, NZ, NZE. rewrite w_spec.(spec_mul).
+intro n; unfold NZtimes, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul).
 rewrite w_spec.(spec_0). now rewrite Zmult_0_r.
 Qed.
 
 Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
 Proof.
-intros n m; unfold NZtimes, NZsucc, NZplus, NZE. rewrite w_spec.(spec_mul).
+intros n m; unfold NZtimes, NZsucc, NZplus, NZeq. rewrite w_spec.(spec_mul).
 rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ).
 rewrite Zplus_mod_idemp_l; [ | apply gt_wB_0]. rewrite Zmult_mod_idemp_r; [ | apply gt_wB_0].
 rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r.