An update on axiomatization of number classes.

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

8 files changed, 142 insertions, 112 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
index 05b8ede94f..6527bd11c3 100644
--- a/theories/Numbers/Integer/Axioms/ZAxioms.v
+++ b/theories/Numbers/Integer/Axioms/ZAxioms.v
@@ -1,14 +1,14 @@
 Require Export ZDomain.
 
 Module Type IntSignature.
-Declare Module Export DomainModule : DomainSignature.
-Open Local Scope ZScope.
+Declare Module Export ZDomainModule : ZDomainSignature.
+Open Local Scope IntScope.
 
 Parameter Inline O : Z.
 Parameter Inline S : Z -> Z.
 Parameter Inline P : Z -> Z.
 
-Notation "0" := O : ZScope.
+Notation "0" := O : IntScope.
 
 Add Morphism S with signature E ==> E as S_wd.
 Add Morphism P with signature E ==> E as P_wd.
@@ -24,9 +24,9 @@ Axiom induction :
 
 End IntSignature.
 
-Module IntProperties (Export IntModule : IntSignature).
-Module Export DomainPropertiesModule := DomainProperties DomainModule.
-Open Local Scope ZScope.
+Module IntProperties (Import IntModule : IntSignature).
+Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule.
+Open Local Scope IntScope.
 
 Ltac induct n :=
   try intros until n;
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index 1a29eddf20..87c99066d0 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -1,6 +1,6 @@
 Require Export NumPrelude.
 
-Module Type DomainSignature.
+Module Type ZDomainSignature.
 
 Parameter Z : Set.
 Parameter E : relation Z.
@@ -15,15 +15,15 @@ Add Relation Z E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Delimit Scope ZScope with Int.
-Bind Scope ZScope with Z.
-Notation "x == y" := (E x y) (at level 70) : ZScope.
-Notation "x # y" := (~ E x y) (at level 70) : ZScope.
+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.
 
-End DomainSignature.
+End ZDomainSignature.
 
-Module DomainProperties (Export DomainModule : DomainSignature).
-Open Local Scope ZScope.
+Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
+Open Local Scope IntScope.
 
 Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
 Proof.
@@ -42,4 +42,4 @@ Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
 
-End DomainProperties.
+End ZDomainProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
index 803bfe43bd..19a66aea3f 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -1,45 +1,45 @@
 Require Export ZAxioms.
 
-Module Type OrderSignature.
+Module Type ZOrderSignature.
 Declare Module Export IntModule : IntSignature.
-Open Local Scope ZScope.
+Open Local Scope IntScope.
 
 Parameter Inline lt : Z -> Z -> bool.
 Parameter Inline le : Z -> Z -> bool.
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
 
-Notation "n <  m" := (lt n m) : ZScope.
-Notation "n <= m" := (le n m) : ZScope.
+Notation "n <  m" := (lt n m) : IntScope.
+Notation "n <= m" := (le n m) : IntScope.
 
 Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irr : forall n, ~ (n < n).
 Axiom lt_S : forall n m, n < (S m) <-> n <= m.
 
-End OrderSignature.
+End ZOrderSignature.
 
 
-Module OrderProperties (Export OrderModule : OrderSignature).
+Module ZOrderProperties (Import ZOrderModule : ZOrderSignature).
 Module Export IntPropertiesModule := IntProperties IntModule.
-Open Local Scope ZScope.
+Open Local Scope IntScope.
 
-Ltac le_intro1 := rewrite le_lt; left.
-Ltac le_intro2 := rewrite le_lt; right.
-Ltac le_elim H := rewrite le_lt in H; destruct H as [H | H].
+Ltac Zle_intro1 := rewrite le_lt; left.
+Ltac Zle_intro2 := rewrite le_lt; right.
+Ltac Zle_elim H := rewrite le_lt in H; destruct H as [H | H].
 
 Theorem le_refl : forall n, n <= n.
 Proof.
-intro n; now le_intro2.
+intro n; now Zle_intro2.
 Qed.
 
 Theorem lt_n_Sn : forall n, n < S n.
 Proof.
-intro n. rewrite lt_S. now le_intro2.
+intro n. rewrite lt_S. now Zle_intro2.
 Qed.
 
 Theorem le_n_Sn : forall n, n <= S n.
 Proof.
-intro; le_intro1; apply lt_n_Sn.
+intro; Zle_intro1; apply lt_n_Sn.
 Qed.
 
 Theorem lt_Pn_n : forall n, P n < n.
@@ -49,17 +49,17 @@ Qed.
 
 Theorem le_Pn_n : forall n, P n <= n.
 Proof.
-intro; le_intro1; apply lt_Pn_n.
+intro; Zle_intro1; apply lt_Pn_n.
 Qed.
 
 Theorem lt_n_Sm : forall n m, n < m -> n < S m.
 Proof.
-intros. rewrite lt_S. now le_intro1.
+intros. rewrite lt_S. now Zle_intro1.
 Qed.
 
 Theorem le_n_Sm : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m H; rewrite <- lt_S in H; now le_intro1.
+intros n m H; rewrite <- lt_S in H; now Zle_intro1.
 Qed.
 
 Theorem lt_n_m_P : forall n m, n < m <-> n <= P m.
@@ -69,7 +69,7 @@ Qed.
 
 Theorem not_le_n_Pn : forall n, ~ n <= P n.
 Proof.
-intros n H; le_elim H.
+intros n H; Zle_elim H.
 apply lt_n_Sm in H; rewrite S_P in H; false_hyp H lt_irr.
 pose proof (lt_Pn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr.
 Qed.
@@ -84,28 +84,28 @@ Proof.
 intro n; induct_n m (P n).
 split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn.
 intros m IH; split; intro H.
-apply -> lt_S in H; le_elim H.
+apply -> lt_S in H; Zle_elim H.
 apply -> IH in H; now apply le_n_Sm.
-rewrite <- H; rewrite S_P; now le_intro2.
+rewrite <- H; rewrite S_P; now Zle_intro2.
 apply -> le_S in H; destruct H as [H | H].
 apply <- IH in H. now apply lt_n_Sm. rewrite H; rewrite P_S; apply lt_n_Sn.
 intros m IH; split; intro H.
 pose proof H as H1. apply lt_n_Sm in H; rewrite S_P in H.
-apply -> IH in H; le_elim H. now apply -> lt_n_m_P.
+apply -> IH in H; Zle_elim H. now apply -> lt_n_m_P.
 rewrite H in H1; false_hyp H1 lt_irr.
 pose proof H as H1. apply le_n_Sm in H. rewrite S_P in H.
-apply <- IH in H. apply -> lt_n_m_P in H. le_elim H.
+apply <- IH in H. apply -> lt_n_m_P in H. Zle_elim H.
 assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn.
 Qed.
 
 Theorem lt_Pn_m : forall n m, n < m -> P n < m.
 Proof.
-intros; rewrite lt_P; now le_intro1.
+intros; rewrite lt_P; now Zle_intro1.
 Qed.
 
 Theorem le_Pn_m : forall n m, n <= m -> P n <= m.
 Proof.
-intros n m H; rewrite <- lt_P in H; now le_intro1.
+intros n m H; rewrite <- lt_P in H; now Zle_intro1.
 Qed.
 
 Theorem lt_n_m_S : forall n m, n < m <-> S n <= m.
@@ -120,7 +120,7 @@ Qed.
 
 Theorem le_Sn_m : forall n m, S n <= m -> n <= m.
 Proof.
-intros n m H; rewrite <- lt_n_m_S in H; now le_intro1.
+intros n m H; rewrite <- lt_n_m_S in H; now Zle_intro1.
 Qed.
 
 Theorem lt_n_Pm : forall n m, n < P m -> n < m.
@@ -130,7 +130,7 @@ Qed.
 
 Theorem le_n_Pm : forall n m, n <= P m -> n <= m.
 Proof.
-intros n m H; rewrite <- lt_n_m_P in H; now le_intro1.
+intros n m H; rewrite <- lt_n_m_P in H; now Zle_intro1.
 Qed.
 
 Theorem lt_respects_S : forall n m, n < m <-> S n < S m.
@@ -185,30 +185,30 @@ Proof.
 intros n m; induct_n n m.
 intros p H _; false_hyp H lt_irr.
 intros n IH p H1 H2. apply lt_Sn_m in H1. pose proof (IH p H1 H2) as H3.
-rewrite lt_n_m_S in H3; le_elim H3.
-assumption. rewrite <- H3 in H2. rewrite lt_S in H2; le_elim H2.
+rewrite lt_n_m_S in H3; Zle_elim H3.
+assumption. rewrite <- H3 in H2. rewrite lt_S in H2; Zle_elim H2.
 elimtype False; apply lt_irr with (n := n); now apply IH.
 rewrite H2 in H1; false_hyp H1 lt_irr.
-intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; le_elim H1.
+intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; Zle_elim H1.
 now apply IH. now rewrite H1.
 Qed.
 
 Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
 Proof.
-intros n m p H1 H2; le_elim H1.
-le_elim H2. le_intro1; now apply lt_trans with (m := m).
-le_intro1; now rewrite <- H2. now rewrite H1.
+intros n m p H1 H2; Zle_elim H1.
+Zle_elim H2. Zle_intro1; now apply lt_trans with (m := m).
+Zle_intro1; now rewrite <- H2. now rewrite H1.
 Qed.
 
 Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
 Proof.
-intros n m p H1 H2; le_elim H1.
+intros n m p H1 H2; Zle_elim H1.
 now apply lt_trans with (m := m). now rewrite H1.
 Qed.
 
 Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
 Proof.
-intros n m p H1 H2; le_elim H2.
+intros n m p H1 H2; Zle_elim H2.
 now apply lt_trans with (m := m). now rewrite <- H2.
 Qed.
 
@@ -219,7 +219,7 @@ Qed.
 
 Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m.
 Proof.
-intros n m H1 H2; le_elim H1; le_elim H2.
+intros n m H1 H2; Zle_elim H1; Zle_elim H2.
 elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m).
 now symmetry. assumption. assumption.
 Qed.
@@ -231,7 +231,7 @@ Qed.
 
 Theorem not_le_Sn_n : forall n, ~ S n <= n.
 Proof.
-intros n H; le_elim H. false_hyp H not_lt_Sn_n.
+intros n H; Zle_elim H. false_hyp H not_lt_Sn_n.
 pose proof (lt_n_Sn n) as H1. rewrite H in H1; false_hyp H1 lt_irr.
 Qed.
 
@@ -357,8 +357,8 @@ intros Qz QS k k_ge_z.
 assert (H : forall n, Q' n). induct_n n z; unfold Q'.
 intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
 intros n IH m H2 H3.
-rewrite lt_S in H3; le_elim H3. now apply IH.
-le_elim H2. rewrite_S_P m.
+rewrite lt_S in H3; Zle_elim H3. now apply IH.
+Zle_elim H2. rewrite_S_P m.
 apply QS. now apply -> lt_n_m_P. apply IH. now apply -> lt_n_m_P.
 rewrite H3; apply lt_Pn_n. now rewrite <- H2.
 intros n IH m H2 H3. apply IH. assumption. now apply lt_n_Pm.
@@ -385,8 +385,8 @@ assert (H : forall n, Q' n). induct_n n z; unfold Q'.
 intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
 intros n IH m H2 H3. apply IH. assumption. now apply lt_Sn_m.
 intros n IH m H2 H3.
-rewrite lt_P in H3; le_elim H3. now apply IH.
-le_elim H2. rewrite_P_S m.
+rewrite lt_P in H3; Zle_elim H3. now apply IH.
+Zle_elim H2. rewrite_P_S m.
 apply QP. now apply -> lt_n_m_S. apply IH. now apply -> lt_n_m_S.
 rewrite H3; apply lt_n_Sn. now rewrite H2.
 pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
@@ -403,9 +403,9 @@ Theorem induction_ord_n :
 Proof.
 intros Qz QS QP n.
 destruct (lt_total n z) as [H | [H | H]].
-now apply left_induction; [| | le_intro1].
+now apply left_induction; [| | Zle_intro1].
 now rewrite H.
-now apply right_induction; [| | le_intro1].
+now apply right_induction; [| | Zle_intro1].
 Qed.
 
 End Center.
@@ -447,5 +447,5 @@ Ltac induct_ord n :=
   let m := fresh "m" in
   let H := fresh "H" in intros n m H; qmorphism n m | | |].
 
-End OrderProperties.
+End ZOrderProperties.
 
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
index 484607094a..6c1f492319 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -1,16 +1,16 @@
 Require Export ZAxioms.
 
-Module Type PlusSignature.
+Module Type ZPlusSignature.
 Declare Module Export IntModule : IntSignature.
-Open Local Scope ZScope.
+Open Local Scope IntScope.
 
 Parameter Inline plus : Z -> Z -> Z.
 Parameter Inline minus : Z -> Z -> Z.
 Parameter Inline uminus : Z -> Z.
 
-Notation "x + y" := (plus x y) : ZScope.
-Notation "x - y" := (minus x y) : ZScope.
-Notation "- x" := (uminus x) : ZScope.
+Notation "x + y" := (plus x y) : IntScope.
+Notation "x - y" := (minus x y) : IntScope.
+Notation "- x" := (uminus x) : IntScope.
 
 Add Morphism plus with signature E ==> E ==> E as plus_wd.
 Add Morphism minus with signature E ==> E ==> E as minus_wd.
@@ -25,11 +25,11 @@ Axiom minus_S : forall n m, n - (S m) == P (n - m).
 Axiom uminus_0 : - 0 == 0.
 Axiom uminus_S : forall n, - (S n) == P (- n).
 
-End PlusSignature.
+End ZPlusSignature.
 
-Module PlusProperties (Export PlusModule : PlusSignature).
+Module ZPlusProperties (Import ZPlusModule : ZPlusSignature).
 Module Export IntPropertiesModule := IntProperties IntModule.
-Open Local Scope ZScope.
+Open Local Scope IntScope.
 
 Theorem plus_P : forall n m, P n + m == P (n + m).
 Proof.
@@ -218,4 +218,4 @@ Proof.
 intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
 Qed.
 
-End PlusProperties.
+End ZPlusProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
index dd311b49ae..946bdf3cb5 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -1,14 +1,13 @@
 Require Export ZOrder.
 Require Export ZPlus.
 
-Module PlusOrderProperties (PlusModule : PlusSignature)
-                           (OrderModule : OrderSignature with
-                             Module IntModule := PlusModule.IntModule).
-(* Warning: Notation _ == _ was already used in scope ZScope !!! *)
-Module Export PlusPropertiesModule := PlusProperties PlusModule.
-Module Export OrderPropertiesModule := OrderProperties OrderModule.
+Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature)
+                            (Import ZOrderModule : ZOrderSignature with
+                              Module IntModule := ZPlusModule.IntModule).
+Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
+Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule.
 (* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *)
-Open Local Scope ZScope.
+Open Local Scope IntScope.
 
 Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
@@ -44,19 +43,19 @@ Qed.
 
 Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
 Proof.
-intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat.
+intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat.
 rewrite H2. now apply -> plus_lt_compat_r.
 Qed.
 
 Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
 Proof.
-intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat.
+intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat.
 rewrite H1. now apply -> plus_lt_compat_l.
 Qed.
 
 Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
 Proof.
-intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat.
+intros n m p q H1 H2. Zle_elim H1. Zle_intro1; now apply plus_lt_le_compat.
 rewrite H1. now apply -> plus_le_compat_l.
 Qed.
 
@@ -71,7 +70,7 @@ induct n.
 induct_ord m.
 intro H; false_hyp H lt_irr.
 intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *.
-le_elim H1. apply IH in H1. now apply lt_Pn_m.
+Zle_elim H1. apply IH in H1. now apply lt_Pn_m.
 rewrite <- H1; rewrite uminus_0; apply lt_Pn_n.
 intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1.
 intros n IH m H. rewrite uminus_S.
@@ -158,4 +157,4 @@ intros n m p. rewrite (minus_le_nondecr_l (n + p) m p).
 rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
 Qed.
 
-End PlusOrderProperties.
+End ZPlusOrderProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index 052dcf66fc..7d4329a963 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -1,12 +1,12 @@
 Require Export ZPlus.
 
-Module Type TimesSignature.
-Declare Module Export PlusModule : PlusSignature.
-Open Local Scope ZScope.
+Module Type ZTimesSignature.
+Declare Module Export ZPlusModule : ZPlusSignature.
+Open Local Scope IntScope.
 
 Parameter Inline times : Z -> Z -> Z.
 
-Notation "x * y" := (times x y) : ZScope.
+Notation "x * y" := (times x y) : IntScope.
 
 Add Morphism times with signature E ==> E ==> E as times_wd.
 
@@ -26,11 +26,11 @@ French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not
 2 + 2 + 2. So it would possibly be more reasonable to define multiplication
 (here as well as in set theory) by recursion on the first argument. *)
 
-End TimesSignature.
+End ZTimesSignature.
 
-Module TimesProperties (Export TimesModule : TimesSignature).
-Module Export PlusPropertiesModule := PlusProperties PlusModule.
-Open Local Scope ZScope.
+Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
+Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
+Open Local Scope IntScope.
 
 Theorem times_P : forall n m, n * (P m) == n * m - n.
 Proof.
@@ -130,4 +130,4 @@ intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH.
 intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH.
 Qed.
 
-End TimesProperties.
+End ZTimesProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
index a72636a420..28c07a99d6 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -1,20 +1,20 @@
 Require Export ZTimes.
 Require Export ZPlusOrder.
 
-Module TimesOrderProperties (TimesModule : TimesSignature)
-                            (OrderModule : OrderSignature with
-                              Module IntModule := TimesModule.PlusModule.IntModule).
-Module Export TimesPropertiesModule := TimesProperties TimesModule.
-Module Export PlusOrderPropertiesModule :=
-  PlusOrderProperties TimesModule.PlusModule OrderModule.
-Open Local Scope ZScope.
+Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature)
+                             (Import ZOrderModule : ZOrderSignature with
+                               Module IntModule := ZTimesModule.ZPlusModule.IntModule).
+Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule.
+Module Export ZPlusOrderPropertiesModule :=
+  ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule.
+Open Local Scope IntScope.
 
 Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p.
 Proof.
 intros n m p; induct_ord p.
 intros H _; false_hyp H lt_irr.
 intros p H IH H1 H2. do 2 rewrite times_S.
-apply -> lt_S in H1; le_elim H1.
+apply -> lt_S in H1; Zle_elim H1.
 apply plus_lt_compat. now apply IH. assumption.
 rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0.
 intros p H IH H1 H2. apply lt_n_Pm in H1. apply -> le_gt in H.
@@ -29,9 +29,9 @@ Qed.
 
 Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p.
 Proof.
-intros n m p H1 H2; le_elim H2.
-le_intro1; now apply mult_lt_compat_r.
-rewrite H2. now le_intro2.
+intros n m p H1 H2; Zle_elim H2.
+Zle_intro1; now apply mult_lt_compat_r.
+rewrite H2. now Zle_intro2.
 Qed.
 
 Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m.
@@ -86,4 +86,4 @@ false_hyp H4 H2.
 apply neq_symm. apply lt_neq. now apply mult_pos_pos.
 Qed.
 
-End TimesOrderProperties.
+End ZTimesOrderProperties.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 2ca4bc5d86..fb4b137d63 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,18 +1,28 @@
-Require Export NTimesLt.
+Require Export NMinus.
+Require Export NTimesOrder.
 Require Export ZTimesOrder.
 
-Module NatPairsDomain (Export NPlusModule : NPlus.PlusSignature) :
-  ZDomain.DomainSignature
-  with Definition Z := (N * N)%type.
-  with Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
-  with Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
+Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
+(*  with Definition Z :=
+    (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type
+  with Definition E :=
+    fun p1 p2  =>
+      NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
+  with Definition e :=
+    fun p1 p2  =>
+      NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
+Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
 
-Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
-Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
+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.
 
 Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
 Proof.
@@ -43,12 +53,12 @@ as E_rel.
 
 End NatPairsDomain.
 
-
-Module NatPairsInt (Export NPlusModule : NPlus.PlusSignature) <: IntSignature.
-
+Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature.
 Module Export ZDomainModule := NatPairsDomain NPlusModule.
+Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule.
+Open Local Scope IntScope.
 
-Definition O := (0, 0).
+Definition O : Z := (0, 0)%Nat.
 Definition S (n : Z) := (NatModule.S (fst n), snd n).
 Definition P (n : Z) := (fst n, NatModule.S (snd n)).
 (* Unfortunately, we do not have P (S n) = n but only P (S n) == n.
@@ -57,6 +67,8 @@ the elements is 0, and make all operations convert canonical values into
 other canonical values. We do not do this because this is more complex
 and because we do not have the predecessor function on N at this point. *)
 
+Notation "0" := O : IntScope.
+
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
@@ -70,6 +82,25 @@ do 2 rewrite plus_n_Sm; now rewrite H.
 Qed.
 
 Theorem S_inj : forall x y : Z, S x == S y -> x == y.
+Proof.
+unfold S, E; simpl; intros x y H.
+do 2 rewrite plus_Sn_m in H. now apply S_inj in H.
+Qed.
+
+Theorem S_P : forall x : Z, S (P x) == x.
+Proof.
+intro x; unfold S, P, E; simpl.
+rewrite plus_Sn_m; now rewrite plus_n_Sm.
+Qed.
+
+Theorem induction :
+  forall Q : Z -> Prop,
+    NumPrelude.pred_wd E Q -> Q 0 ->
+    (forall x, Q x -> Q (S x)) ->
+    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+Proof.
+intros Q Q_wd Q0 QS QP x; unfold O, S, P in *.
+