An update on axiomatic number classes.

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

19 files changed, 765 insertions, 498 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index 87c99066d..579f8face 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -2,9 +2,9 @@ Require Export NumPrelude.
 
 Module Type ZDomainSignature.
 
-Parameter Z : Set.
-Parameter E : relation Z.
-Parameter e : Z -> Z -> bool.
+Parameter Inline Z : Set.
+Parameter Inline E : 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.
@@ -42,4 +42,14 @@ Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
 
+Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step ZE_stepl.
+
+(* The right step lemma is just transitivity of E *)
+Declare Right Step (proj1 (proj2 E_equiv)).
+
 End ZDomainProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index 7d4329a96..5dc0b7505 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -13,19 +13,6 @@ Add Morphism times with signature E ==> E ==> E as times_wd.
 Axiom times_0 : forall n, n * 0 == 0.
 Axiom times_S : forall n m, n * (S m) == n * m + n.
 
-(* Here recursion is done on the second argument to conform to the
-usual definition of ordinal multiplication in set theory, which is not
-commutative. It seems, however, that this definition in set theory is
-unfortunate for two reasons. First, multiplication of two ordinals A
-and B can be defined as (an order type of) the cartesian product B x A
-(not A x B) ordered lexicographically. For example, omega * 2 =
-2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...},
-while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) <
-(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in
-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 ZTimesSignature.
 
 Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index 5f592dbcb..683b86ec6 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -1,5 +1,5 @@
-Require Export NTimesOrder.
-Require Export ZTimesOrder.
+Require Import NPlus.
+Require Export ZAxioms.
 
 Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
 (*  with Definition Z :=
@@ -11,7 +11,7 @@ Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
     fun p1 p2  =>
       NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
 Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
@@ -28,26 +28,35 @@ Proof.
 intros x y; unfold E, e; apply E_equiv_e.
 Qed.
 
-Theorem E_equiv : equiv Z E.
+Theorem ZE_refl : reflexive Z E.
+Proof.
+unfold reflexive, E; reflexivity.
+Qed.
+
+Theorem ZE_symm : symmetric Z E.
 Proof.
-split; [| split]; unfold reflexive, symmetric, transitive, E.
-(* reflexivity *)
-now intro.
-(* transitivity *)
-intros x y z H1 H2.
+unfold symmetric, E; now symmetry.
+Qed.
+
+Theorem ZE_trans : transitive Z E.
+Proof.
+unfold transitive, E. intros x y z H1 H2.
 apply plus_cancel_l with (p := fst y + snd y).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
 rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
 rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
-(* symmetry *)
-now intros.
 Qed.
 
-Add Relation Z E                                                                                 
- reflexivity proved by (proj1 E_equiv)                                                           
- symmetry proved by (proj2 (proj2 E_equiv))                                                      
- transitivity proved by (proj1 (proj2 E_equiv))                                                  
+Theorem E_equiv : equiv Z E.
+Proof.
+unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]].
+Qed.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
 Add Morphism (@pair N N)
@@ -78,25 +87,25 @@ Notation "0" := O : IntScope.
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
-do 2 rewrite plus_Sn_m; now rewrite H.
+do 2 rewrite plus_S_l; now rewrite H.
 Qed.
 
 Add Morphism P with signature E ==> E as P_wd.
 Proof.
 unfold P, E; intros n m H; simpl.
-do 2 rewrite plus_n_Sm; now rewrite H.
+do 2 rewrite plus_S_r; 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.
+do 2 rewrite plus_S_l 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.
+rewrite plus_S_l; now rewrite plus_S_r.
 Qed.
 
 Section Induction.
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
new file mode 100644
index 000000000..29181e0c6
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
@@ -0,0 +1,111 @@
+Require Import NPlusOrder.
+Require Export ZPlusOrder.
+Require Export ZPairsPlus.
+
+Module NatPairsOrder (Import NPlusModule : NPlusSignature)
+                     (Import NOrderModule : NOrderSignature
+                        with Module NatModule := NPlusModule.NatModule) <: ZOrderSignature.
+Module Import NPlusOrderPropertiesModule :=
+  NPlusOrderProperties NPlusModule NOrderModule.
+Module Export IntModule := NatPairsInt NPlusModule.
+Open Local Scope NatScope.
+
+Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1).
+Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1).
+
+Notation "x < y" := (lt x y) : IntScope.
+Notation "x <= y" := (le x y) : IntScope.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff; split; intro H.
+stepr (snd y1 + fst y2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption].
+stepl (snd y2 + fst x1) by apply plus_comm.
+stepr (fst y2 + snd x1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd x2) (fst x2)).
+now stepl (fst x1 + snd x2) by apply plus_comm.
+stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm.
+stepr (snd x1 + fst x2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry].
+stepl (snd x2 + fst y1) by apply plus_comm.
+stepr (fst x2 + snd y1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd y2) (fst y2)).
+now stepl (fst y1 + snd y2) by apply plus_comm.
+stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm.
+Qed.
+
+(* Below is a very long explanation why it would be useful to be
+able to use the fold tactic in hypotheses.
+We will prove the following statement not from scratch, like lt_wd,
+but expanding <= to < and == and then using lt_wd. The theorem we need
+to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z.
+To be able to express <= through < and ==, we need to expand <=%Int to
+<=%Nat, since we have not proved yet the properties of <=%Int. But
+then it would be convenient to fold back equalities from
+(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int.
+The reason is that we will need to show that (x1 == x2)%Int <->
+(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold
+equalities back to Int, then we could do simple rewriting, since we have
+already showed that ==%Int is an equivalence relation. On the other hand,
+if we leave equalities expanded to Nat, we will have to apply the
+transitivity of ==%Int by hand. *)
+
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff. do 2 rewrite le_lt.
+pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H.
+(* This is a remark about an extra level of definitions created by
+"with Module NatModule := NPlusModule.NatModule" constraint in the beginning
+of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
+that it expand to (NPlusModule.NatModule.NDomainModule.E ... ...), since
+NPlusModule was imported first. On the other hand, the goal uses
+NOrderModule.NatModule.NDomainModule.E, or just NDomainModule.E, since le_lt
+theorem was proved in NOrderDomain module. (E without qualifiers refers to
+ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer,
+though, if the constraint "with Module NatModule := NPlusModule.NatModule" in the
+declaration of this functor would not create an extra level of definitions
+and there would be only one NDomainModule.E. *)
+replace NDomainModule.E with NPlusModule.NatModule.NDomainModule.E by reflexivity.
+fold (x1 == x2)%Int. fold (y1 == y2)%Int.
+assert (H1' : (x1 == y1)%Int); [exact H1 |].
+(* We do this instead of "fold (x1 == y1)%Int in H1" *)
+assert (H2' : (x2 == y2)%Int); [exact H2 |].
+rewrite H1'; rewrite H2'. reflexivity.
+Qed.
+
+Open Local Scope IntScope.
+
+Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *)
+Qed.
+
+Theorem lt_irr : forall n : Z, ~ (n < n).
+Proof.
+intros n; unfold lt, E; simpl. apply lt_irr.
+(* refers to NPlusOrderPropertiesModule.NOrderPropertiesModule.lt_irr *)
+Qed.
+
+Theorem lt_S : forall n m, n < (S m) <-> n <= m.
+Proof.
+intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S.
+Qed.
+
+End NatPairsOrder.
+
+(* Since to define the order on integers we need both plus and order
+on natural numbers, we can export the properties of plus and order together *)
+(*Module NatPairsPlusOrderProperties (NPlusModule : NPlusSignature)
+                                   (NOrderModule : NOrderSignature
+                                     with Module NatModule := NPlusModule.NatModule).
+Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module Export NatPairsOrderModule := NatPairsOrder NPlusModule NOrderModule.
+Module Export NatPairsPlusOrderPropertiesModule :=
+  ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
+End NatPairsPlusOrderProperties.*)
+(* We cannot prove to Coq that NatPairsPlusModule.IntModule and
+NatPairsOrderModule.IntModule are the same *)
+
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
index b69e4ce7d..d18076265 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
@@ -1,6 +1,6 @@
-Require Export NTimesOrder.
-Require Export ZTimesOrder.
-Require Import ZPairsAxioms.
+Require Import NPlus.
+Require Export ZPlus.
+Require Export ZPairsAxioms.
 
 Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature.
 Module Export IntModule := NatPairsInt NPlusModule.
@@ -46,12 +46,12 @@ Open Local Scope IntScope.
 
 Theorem plus_0 : forall n, 0 + n == n.
 Proof.
-intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_n.
+intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_l.
 Qed.
 
 Theorem plus_S : forall n m, (S n) + m == S (n + m).
 Proof.
-intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_Sn_m.
+intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_S_l.
 Qed.
 
 Theorem minus_0 : forall n, n - 0 == n.
@@ -61,12 +61,12 @@ Qed.
 
 Theorem minus_S : forall n m, n - (S m) == P (n - m).
 Proof.
-intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_n_Sm.
+intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_S_r.
 Qed.
 
 Theorem uminus_0 : - 0 == 0.
 Proof.
-unfold uminus, E; simpl. now rewrite plus_0_n.
+unfold uminus, E; simpl. now rewrite plus_0_l.
 Qed.
 
 Theorem uminus_S : forall n, - (S n) == P (- n).
@@ -77,6 +77,6 @@ Qed.
 End NatPairsPlus.
 
 Module NatPairsPlusProperties (NPlusModule : NPlusSignature).
-Module NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
 Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
 End NatPairsPlusProperties.
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
index f5706276c..b72847c08 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
@@ -1,12 +1,14 @@
+Require Import Ring.
+Require Import NTimes.
+Require Export ZTimes.
 Require Export ZPairsPlus.
 
 Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature.
-Module Import ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
+Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
+Module Import NTimesPropertiesModule := NTimesProperties NTimesModule.
 Open Local Scope NatScope.
 
 Definition times (n m : Z) :=
-(*  let (n1, n2) := n in
-  let (m1, m2) := m in (n1 * m1 + n2 * m2, n1 * m2 + n2 * m1).*)
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
 
 Notation "x * y" := (times x y) : IntScope.
@@ -14,24 +16,40 @@ Notation "x * y" := (times x y) : IntScope.
 Add Morphism times with signature E ==> E ==> E as times_wd.
 Proof.
 unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl.
-assert ((fst x1) + (fst y1) == (fst y1) + (fst x1)).
+stepl_ring (fst x1 * fst x2 + (snd x1 * snd x2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (fst x1 * snd x2 + (fst y1 * fst y2 + snd y1 * snd y2 + snd x1 * fst x2)).
+apply plus_times_repl_pair with (n := fst y2) (m := snd y2); [| now idtac].
+stepl_ring (snd x1 * snd x2 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (snd x1 * fst x2 + (fst x1 * snd y2 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := snd y2) (m := fst y2);
+  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
+stepl_ring (snd y2 * snd x1 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (snd y2 * fst x1 + (snd x1 * fst y2 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := snd y1) (m := fst y1);
+  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
+stepl_ring (fst y2 * fst x1 + (snd y2 * snd y1 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (fst y2 * snd x1 + (snd y2 * fst y1 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := fst y1) (m := snd y1); [| now idtac].
 ring.
+Qed.
 
+Open Local Scope IntScope.
 
-Axiom times_0 : forall n, n * 0 == 0.
-Axiom times_S : forall n m, n * (S m) == n * m + n.
+Theorem times_0 : forall n, n * 0 == 0.
+Proof.
+intro n; unfold times, E; simpl.
+repeat rewrite times_0_r. now rewrite plus_assoc.
+Qed.
+
+Theorem times_S : forall n m, n * (S m) == n * m + n.
+Proof.
+intros n m; unfold times, S, E; simpl.
+do 2 rewrite times_S_r. ring.
+Qed.
 
-(* Here recursion is done on the second argument to conform to the
-usual definition of ordinal multiplication in set theory, which is not
-commutative. It seems, however, that this definition in set theory is
-unfortunate for two reasons. First, multiplication of two ordinals A
-and B can be defined as (an order type of) the cartesian product B x A
-(not A x B) ordered lexicographically. For example, omega * 2 =
-2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...},
-while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) <
-(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in
-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 NatPairsTimes.
 
-End ZTimesSignature.
+Module NatPairsTimesProperties (NTimesModule : NTimesSignature).
+Module Export NatPairsTimesModule := NatPairsTimes NTimesModule.
+Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
+End NatPairsTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index da4c0af3d..ceccf840a 100644
--- a/theories/Numbers/Natural/Axioms/NAxioms.v
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -16,7 +16,7 @@ not make sense to get unqualified access to O and S but not to N. *)
 Open Local Scope NatScope.
 
 Parameter Inline O : N.
-Parameter Inline S : N -> N.
+Parameter (*Inline*) S : N -> N.
 
 Notation "0" := O : NatScope.
 Notation "1" := (S O) : NatScope.
@@ -174,14 +174,21 @@ Implicit Arguments recursion_S [A].
 
 End NatSignature.
 
-(* We would like to have a signature for the predecessor: first, to be
-able to provide an efficient implementation, and second, to be able to
-use this function in the signatures defining other functions, e.g.,
-subtraction. If we just define predecessor by recursion in
-NatProperties functor, we would not be able to use it in other
-signatures. We cannot put the functor NDefPred below in a different
-file because the definition of the predecessor uses recursion and the
-proof of injectivity of the successor uses the predecessor. *)
+(* We use the predecessor function to prove the injectivity of S. There
+are two ways to get this function: define it by primitive recursion, or
+declare a signature and allow the user to provide an implementation,
+similar to how this is done to plus, times, etc. We would like to use
+the first option: first, to allow the user to provide an efficient
+implementation, and second, to be able to use predecessor in signatures
+defining other functions, e.g., subtraction. If we just define
+predecessor by recursion in the NatProperties functor, we would not be
+able to use it in other signatures, since those signatures do not invoke
+the NatProperties functor. After giving a signature for the predecessor,
+we define the functor NDefPred, which defines an implementation of a
+predecessor by primitive recursion. We cannot put NDefPred in a
+different file because the definition of the predecessor uses recursion,
+which is introduced in this file, and the proof of injectivity of the
+successor (also in this file) uses the predecessor. *)
 
 Module Type NPredSignature.
 Declare Module Export NatModule : NatSignature.
@@ -235,6 +242,21 @@ Ltac induct n :=
   let m := fresh "m" in
   let H := fresh "H" in intros n m H; qmorphism n m | |].
 
+Theorem nondep_induction :
+  forall P : N -> Prop, NumPrelude.pred_wd E P ->
+    P 0 -> (forall n, P (S n)) -> forall n, P n.
+Proof.
+intros; apply induction; auto.
+Qed.
+
+Ltac nondep_induct n :=
+  try intros until n;
+  pattern n; apply nondep_induction; clear n;
+  [unfold NumPrelude.pred_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | |].
+
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
@@ -278,16 +300,52 @@ setoid_replace n with (P (S n)) by (symmetry; apply P_S).
 now apply P_wd.
 Qed.
 
-Theorem not_eq_S : forall n m, n # m -> S n # S m.
+Theorem S_inj_contrap : forall n m, n # m -> S n # S m.
 Proof.
 intros n m H1 H2. apply S_inj in H2. now apply H1.
 Qed.
 
-Theorem not_eq_Sn_n : forall n, S n # n.
+Definition iter_S (k : nat) (n : N) :=
+  nat_rec (fun _ => N) n (fun _ p => S p) k.
+
+Add Morphism iter_S with signature (@eq nat) ==> E ==> E as iter_S_wd.
+Proof.
+intros k n m; induction k as [| k IH]; simpl in *.
+trivial.
+intro; apply S_wd; now apply IH.
+Qed.
+
+Theorem iter_S_S : forall (k : nat) (n : N), iter_S k (S n) == S (iter_S k n).
+Proof.
+now (intros k n; induction k; simpl); [| apply S_wd].
+Qed.
+
+Theorem iter_S_neq_0 : forall k : nat, iter_S (Datatypes.S k) 0 # 0.
+Proof.
+destruct k; simpl; apply S_0.
+Qed.
+
+Theorem iter_S_neq : forall (k : nat) (n : N), iter_S (Datatypes.S k) n # n.
 Proof.
-induct n.
+intro k; induct n; simpl.
 apply S_0.
-intros n IH H. apply S_inj in H. now apply IH.
+intros n IH H. apply S_inj in H. apply IH. now rewrite <- iter_S_S.
+Qed.
+
+Theorem S_neq : forall n, S n # n.
+Proof.
+intro n; apply (iter_S_neq 0 n).
+(* "apply iter_S_neq with (k := 0) (n := n)" does not work here !!! *)
+Qed.
+
+Theorem SS_neq : forall n, S (S n) # n.
+Proof.
+intro n; apply (iter_S_neq 1 n).
+Qed.
+
+Theorem SSS_neq : forall n, S (S (S n)) # n.
+Proof.
+intro n; apply (iter_S_neq 2 n).
 Qed.
 
 Theorem not_all_eq_0 : ~ forall n, n == 0.
@@ -302,21 +360,6 @@ induct n; [intro H; now elim H | intros n _ _; now exists n].
 intro H; destruct H as [m H]; rewrite H; apply S_0.
 Qed.
 
-Theorem nondep_induction :
-  forall P : N -> Prop, NumPrelude.pred_wd E P ->
-    P 0 -> (forall n, P (S n)) -> forall n, P n.
-Proof.
-intros; apply induction; auto.
-Qed.
-
-Ltac nondep_induct n :=
-  try intros until n;
-  pattern n; apply nondep_induction; clear n;
-  [unfold NumPrelude.pred_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | |].
-
 Theorem O_or_S : forall n, n == 0 \/ exists m, n == S m.
 Proof.
 nondep_induct n; [now left | intros n; right; now exists n].
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
index c525db3d2..de261bfbe 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -50,8 +50,8 @@ use E instead of = in our formulas. *)
 Proof.
 intros m n; pattern m; apply dep_recursion; clear m.
 intro H.
-rewrite plus_0_n in H. left; now split.
-intros m IH H. rewrite plus_Sn_m in H. apply S_inj in H.
+rewrite plus_0_l in H. left; now split.
+intros m IH H. rewrite plus_S_l in H. apply S_inj in H.
 apply plus_eq_0 in H. destruct H as [H1 H2].
 right; now split; [rewrite H1 |].
 Qed.
@@ -65,7 +65,7 @@ intros; left; reflexivity.
 intros; left; reflexivity.
 intros; right; reflexivity.
 intros n _ m _ H.
-rewrite times_Sn_m in H; rewrite plus_Sn_m in H; now apply S_0 in H.
+rewrite times_S_l in H. rewrite plus_S_r in H; now apply S_0 in H.
 Qed.
 
 End NDepRecTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
index 5b3fde2c2..52148cd38 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -1,9 +1,10 @@
+Require Import Ring.
 Require Export NumPrelude.
 
 Module Type NDomainSignature.
 
 Parameter Inline N : Set.
-Parameter Inline E : relation N.
+Parameter Inline E : N -> N -> Prop.
 Parameter Inline e : N -> N -> bool.
 
 (* Theoretically, we it is enough to have decidable equality e only.
@@ -65,6 +66,11 @@ Module NDomainProperties (Import NDomainModule : NDomainSignature).
 (* It also accepts module of type NatDomainEq *)
 Open Local Scope NatScope.
 
+Theorem Zneq_symm : forall n m, n # m -> m # n.
+Proof.
+intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+Qed.
+
 (* The following easily follows from transitivity of e and E, but
 we need to deal with the coercion *)
 Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
@@ -79,4 +85,17 @@ assert (x == y); [rewrite Exx'; now rewrite Eyy' |
 rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
 Qed.
 
+Theorem NE_stepl : forall x y z : N, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step NE_stepl.
+
+(* The right step lemma is just transitivity of E *)
+Declare Right Step (proj1 (proj2 E_equiv)).
+
+Ltac stepl_ring t := stepl t; [| ring].
+Ltac stepr_ring t := stepr t; [| ring].
+
 End NDomainProperties.
diff --git a/theories/Numbers/Natural/Axioms/NMinus.v b/theories/Numbers/Natural/Axioms/NMinus.v
index 1f112a7b4..70fd8c719 100644
--- a/theories/Numbers/Natural/Axioms/NMinus.v
+++ b/theories/Numbers/Natural/Axioms/NMinus.v
@@ -71,7 +71,7 @@ Proof.
 intros n m H; pattern n, m; apply le_ind_rel.
 unfold rel_wd; intros x x' H1 y y' H2; rewrite H1; now rewrite H2.
 intro; rewrite minus_0_r; now rewrite plus_0_r.
-clear n m H. intros n m _ H2. rewrite minus_comm_S. rewrite plus_n_Sm.
+clear n m H. intros n m _ H2. rewrite minus_comm_S. rewrite plus_S_r.
 now rewrite H2.
 assumption.
 Qed.
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 12cecca18..8743f5961 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -42,16 +42,15 @@ Qed.
 (*****************************************************)
 (**                  Multiplication                  *)
 
-Definition times (x y : N) := recursion 0 (fun x p => plus y p) x.
+Definition times (x y : N) := recursion 0 (fun _ p => plus p x) y.
 
-Lemma times_step_wd : forall y, fun2_wd E E E (fun x p => plus y p).
+Lemma times_step_wd : forall x, fun2_wd E E E (fun _ p => plus p x).
 Proof.
-unfold fun2_wd. intros y _ _ _ p p' Ezz'.
-now apply plus_wd.
+unfold fun2_wd. intros. now apply plus_wd.
 Qed.
 
 Lemma times_step_equal :
-  forall y y', y == y' -> eq_fun2 E E E (fun x p => plus y p) (fun x p => plus y' p).
+  forall x x', x == x' -> eq_fun2 E E E (fun _ p => plus p x) (fun x p => plus p x').
 Proof.
 unfold eq_fun2; intros; apply plus_wd; assumption.
 Qed.
@@ -64,12 +63,12 @@ apply recursion_wd with (EA := E).
 reflexivity. apply times_step_equal. assumption. assumption.
 Qed.
 
-Theorem times_0 : forall y, times 0 y == 0.
+Theorem times_0_r : forall x, times x 0 == 0.
 Proof.
-intro y. unfold times. now rewrite recursion_0.
+intro. unfold times. now rewrite recursion_0.
 Qed.
 
-Theorem times_S : forall x y, times (S x) y == plus y (times x y).
+Theorem times_S_r : forall x y, times x (S y) == plus (times x y) x.
 Proof.
 intros x y; unfold times.
 now rewrite (recursion_S E); [| apply times_step_wd |].
@@ -91,7 +90,7 @@ Definition le (n m : N) := lt n m || e n m.
 Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m.
 Proof.
 intros n m. rewrite E_equiv_e. unfold le.
-do 3 rewrite eq_true_unfold.
+do 3 rewrite eq_true_unfold_pos.
 assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true).
 split; [apply orb_prop | apply orb_true_intro].
 now rewrite H.
@@ -329,12 +328,12 @@ Proof.
 exact plus_wd.
 Qed.
 
-Theorem plus_0_n : forall n, plus 0 n == n.
+Theorem plus_0_l : forall n, plus 0 n == n.
 Proof.
 exact plus_0.
 Qed.
 
-Theorem plus_Sn_m : forall n m, plus (S n) m == S (plus n m).
+Theorem plus_S_l : forall n m, plus (S n) m == S (plus n m).
 Proof.
 exact plus_S.
 Qed.
@@ -351,15 +350,8 @@ Proof.
 exact times_wd.
 Qed.
 
-Theorem times_0_n : forall n, times 0 n == 0.
-Proof.
-exact times_0.
-Qed.
-
-Theorem times_Sn_m : forall n m, times (S n) m == plus m (times n m).
-Proof.
-exact times_S.
-Qed.
+Definition times_0_r := times_0_r.
+Definition times_S_r := times_S_r.
 
 End NDefaultTimesModule.
 
diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v
index 08a6d44a8..1b631ce64 100644
--- a/theories/Numbers/Natural/Axioms/NOrder.v
+++ b/theories/Numbers/Natural/Axioms/NOrder.v
@@ -28,6 +28,31 @@ 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].
 
+Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Declare Left  Step lt_stepl.
+Declare Right Step lt_stepr.
+Declare Left  Step le_stepl.
+Declare Right Step le_stepr.
+
 Theorem le_refl : forall n, n <= n.
 Proof.
 intro; now le_intro2.
@@ -223,11 +248,11 @@ intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |].
 now destruct A as [A | A]; [elim H | right].
 Qed.
 
-Theorem lt_exists_pred : forall n, 0 < n -> exists m, n == S m.
+Theorem lt_exists_pred : forall n m, m < n -> exists p, n == S p.
 Proof.
-induct n.
-intro H; false_hyp H lt_0.
-intros n IH H; now exists n.
+nondep_induct n.
+intros m H; false_hyp H lt_0.
+intros n _ _; now exists n.
 Qed.
 
 (** Elimination principles for < and <= *)
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index d49794d28..3a7c19b62 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -4,48 +4,56 @@ Module Type NPlusSignature.
 Declare Module Export NatModule : NatSignature.
 Open Local Scope NatScope.
 
-Parameter Inline plus : N -> N -> N.
+Parameter (*Inline*) plus : N -> N -> N.
 
 Notation "x + y" := (plus x y) : NatScope.
 
 Add Morphism plus with signature E ==> E ==> E as plus_wd.
 
-Axiom plus_0_n : forall n, 0 + n == n.
-Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m).
+Axiom plus_0_l : forall n, 0 + n == n.
+Axiom plus_S_l : forall n m, (S n) + m == S (n + m).
 
 End NPlusSignature.
 
-Module NPlusProperties (Import NPlusModule : NPlusSignature).
+Module NPlusProperties
+  (NatMod : NatSignature)
+  (Import NPlusModule : NPlusSignature with Module NatModule := NatMod).
 Module Export NatPropertiesModule := NatProperties NatModule.
+Import NatMod.
 Open Local Scope NatScope.
 
+(* If H1 : t1 == u1 and H2 : t2 == u2 then "add_equations H1 H2 as H3"
+adds the hypothesis H3 : t1 + t2 == u1 + u2 *)
+Tactic Notation "add_equations" constr(H1) constr(H2) "as" ident(H3) :=
+match (type of H1) with
+| ?t1 == ?u1 => match (type of H2) with
+              | ?t2 == ?u2 => pose proof (plus_wd t1 u1 H1 t2 u2 H2) as H3
+              | _ => fail 2 ":" H2 "is not an equation"
+              end
+| _ => fail 1 ":" H1 "is not an equation"
+end.
+
 Theorem plus_0_r : forall n, n + 0 == n.
 Proof.
 induct n.
-now rewrite plus_0_n.
+now rewrite plus_0_l.
 intros x IH.
-rewrite plus_Sn_m.
+rewrite plus_S_l.
 now rewrite IH.
 Qed.
 
-Theorem plus_0_l : forall n, 0 + n == n.
-Proof.
-intro n.
-now rewrite plus_0_n.
-Qed.
-
-Theorem plus_n_Sm : forall n m, n + S m == S (n + m).
+Theorem plus_S_r : forall n m, n + S m == S (n + m).
 Proof.
 intros n m; generalize n; clear n. induct n.
-now repeat rewrite plus_0_n.
+now repeat rewrite plus_0_l.
 intros x IH.
-repeat rewrite plus_Sn_m; now rewrite IH.
+repeat rewrite plus_S_l; now rewrite IH.
 Qed.
 
-Theorem plus_Sn_m : forall n m, S n + m == S (n + m).
+Theorem plus_S_l : forall n m, S n + m == S (n + m).
 Proof.
 intros.
-now rewrite plus_Sn_m.
+now rewrite plus_S_l.
 Qed.
 
 Theorem plus_comm : forall n m, n + m == m + n.
@@ -53,7 +61,7 @@ Proof.
 intros n m; generalize n; clear n. induct n.
 rewrite plus_0_l; now rewrite plus_0_r.
 intros x IH.
-rewrite plus_Sn_m; rewrite plus_n_Sm; now rewrite IH.
+rewrite plus_S_l; rewrite plus_S_r; now rewrite IH.
 Qed.
 
 Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
@@ -61,7 +69,7 @@ Proof.
 intros n m p; generalize n; clear n. induct n.
 now repeat rewrite plus_0_l.
 intros x IH.
-repeat rewrite plus_Sn_m; now rewrite IH.
+repeat rewrite plus_S_l; now rewrite IH.
 Qed.
 
 Theorem plus_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q).
@@ -81,7 +89,7 @@ Qed.
 
 Theorem plus_1_l : forall n, 1 + n == S n.
 Proof.
-intro n; rewrite plus_Sn_m; now rewrite plus_0_n.
+intro n; rewrite plus_S_l; now rewrite plus_0_l.
 Qed.
 
 Theorem plus_1_r : forall n, n + 1 == S n.
@@ -92,8 +100,8 @@ Qed.
 Theorem plus_cancel_l : forall n m p, p + n == p + m -> n == m.
 Proof.
 induct p.
-do 2 rewrite plus_0_n; trivial.
-intros p IH H. do 2 rewrite plus_Sn_m in H. apply S_inj in H. now apply IH.
+do 2 rewrite plus_0_l; trivial.
+intros p IH H. do 2 rewrite plus_S_l in H. apply S_inj in H. now apply IH.
 Qed.
 
 Theorem plus_cancel_r : forall n m p, n + p == m + p -> n == m.
@@ -107,8 +115,8 @@ Qed.
 Theorem plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
-rewrite plus_0_n; now split.
-intros n IH H. rewrite plus_Sn_m in H.
+rewrite plus_0_l; now split.
+intros n IH H. rewrite plus_S_l in H.
 absurd_hyp H; [|assumption]. unfold not; apply S_0.
 Qed.
 
@@ -124,28 +132,10 @@ Theorem succ_plus_discr : forall n m, m # S (n + m).
 Proof.
 intro n; induct m.
 intro H. apply S_0 with (n := (n + 0)). now apply (proj2 (proj2 E_equiv)). (* symmetry *)
-intros m IH H. apply S_inj in H. rewrite plus_n_Sm in H.
+intros m IH H. apply S_inj in H. rewrite plus_S_r in H.
 unfold not in IH; now apply IH.
 Qed.
 
-Theorem n_SSn : forall n, n # S (S n).
-Proof.
-intro n. pose proof (succ_plus_discr 1 n) as H.
-rewrite plus_Sn_m in H; now rewrite plus_0_n in H.
-Qed.
-
-Theorem n_SSSn : forall n, n # S (S (S n)).
-Proof.
-intro n. pose proof (succ_plus_discr (S (S 0)) n) as H.
-do 2 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
-Qed.
-
-Theorem n_SSSSn : forall n, n # S (S (S (S n))).
-Proof.
-intro n. pose proof (succ_plus_discr (S (S (S 0))) n) as H.
-do 3 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
-Qed.
-
 (* The following section is devoted to defining a function that, given
 two numbers whose some equals 1, decides which number equals 1. The
 main property of the function is also proved .*)
@@ -154,8 +144,8 @@ main property of the function is also proved .*)
 Theorem plus_eq_1 :
   forall m n, m + n == 1 ->  (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0).
 induct m.
-intros n H; rewrite plus_0_n in H; left; now split.
-intros n IH m H; rewrite plus_Sn_m in H; apply S_inj in H;
+intros n H; rewrite plus_0_l in H; left; now split.
+intros n IH m H; rewrite plus_S_l in H; apply S_inj in H;
 apply plus_eq_0 in H; destruct H as [H1 H2];
 now right; split; [apply S_wd |].
 Qed.
@@ -201,7 +191,7 @@ rewrite plus_eq_1_dec_0.
 split; [intros; now split | intro H1; discriminate H1].
 intros m _ H. rewrite plus_eq_1_dec_S.
 split; [intro H1; discriminate | intros _ ].
-rewrite plus_Sn_m in H. apply S_inj in H.
+rewrite plus_S_l in H. apply S_inj in H.
 apply plus_eq_0 in H; split; [apply S_wd | ]; tauto.
 Qed.
 
@@ -231,47 +221,9 @@ intros n IH.
 (* destruct IH as [p H | p H]. does not print a goal in ProofGeneral *)
 destruct IH as [[p H] | [p H]].
 destruct (O_or_S p) as [H1 | [p' H1]]; rewrite H1 in H.
-rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_Sn_m; now rewrite plus_0_l.
-left; exists p'; rewrite plus_n_Sm; now rewrite plus_Sn_m in H.
-right; exists (S p). rewrite plus_Sn_m; now rewrite H.
+rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_S_l; now rewrite plus_0_l.
+left; exists p'; rewrite plus_S_r; now rewrite plus_S_l in H.
+right; exists (S p). rewrite plus_S_l; now rewrite H.
 Qed.
 
-(* In proving the correctness of the definition of multiplication on
-integers constructed from pairs of natural numbers, we'll need the
-following fact about natural numbers:
-
-a * x + u == a * y + v -> x + y' == x' + y -> a * x' + u = a * y' + v  (2)
-
-Here x + y' == x' + y represents equality of integers (x, y) and
-(x', y'), since a pair of natural numbers represents their integer
-difference. On integers, the (2) could be proved by moving
-a * y to the left, factoring out a and replacing x - y by x' - y'.
-However, the whole point is that we are only in the process of
-constructing integers, so this has to be proved for natural numbers,
-where we cannot move terms from one side of an equation to the other.
-We first prove the special case of (2) where a == 1. *)
-
-Theorem plus_repl_pair : forall n m n' m' u v,
-  n + u == m + v -> n + m' == n' + m -> n' + u == m' + v.
-Proof.
-induct n.
-intros m n' m' u v H1 H2. rewrite plus_0_l in H1. rewrite plus_0_l in H2.
-rewrite H1; rewrite H2. now rewrite plus_assoc.
-intros n IH m n' m' u v H1 H2. rewrite plus_Sn_m in H1. rewrite plus_Sn_m in H2.
-assert (H : (exists m'', m == S m'') \/ ((exists v', v == S v') /\ (exists n'', n' == S n''))).
-symmetry in H1; symmetry in H2;
-destruct (plus_eq_S m v (n + u) H1); destruct (plus_eq_S n' m (n + m') H2).
-now left. now left. right; now split. now left.
-(* destruct H as [[m'' H] | [v' H3] [n'' H4]]. *)
-(* The command above produces a warning and the PG does not show a goal !!! *) 
-destruct H as [[m'' H] | [[v' H3] [n'' H4]]].
-rewrite H in H1, H2. rewrite plus_Sn_m in H1; rewrite plus_n_Sm in H2.
-apply S_inj in H1; apply S_inj in H2. now apply (IH m'').
-rewrite H3; rewrite H4; rewrite plus_Sn_m; rewrite plus_n_Sm; apply S_wd.
-rewrite H3 in H1; rewrite H4 in H2; rewrite plus_Sn_m in H2; rewrite plus_n_Sm in H1;
-apply S_inj in H1; apply S_inj in H2. now apply (IH m).
-Qed.
-
-(* The formula (2) will be proved in NTimes.v *)
-
 End NPlusProperties.
diff --git a/theories/Numbers/Natural/Axioms/NPlusOrder.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v
index d152a0368..4119e3c24 100644
--- a/theories/Numbers/Natural/Axioms/NPlusOrder.v
+++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v
@@ -4,7 +4,7 @@ Require Export NOrder.
 Module NPlusOrderProperties (Import NPlusModule : NPlusSignature)
                          (Import NOrderModule : NOrderSignature with
                            Module NatModule := NPlusModule.NatModule).
-Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
 Module Export NOrderPropertiesModule := NOrderProperties NOrderModule.
 Open Local Scope NatScope.
 
@@ -14,37 +14,69 @@ Proof.
 intros n m p; induct p.
 now rewrite plus_0_r.
 intros x IH H.
-rewrite plus_n_Sm. apply lt_closed_S. apply IH; apply H.
+rewrite plus_S_r. apply lt_closed_S. apply IH; apply H.
 Qed.
 
-Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
+Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
 Proof.
 intros n m p H; induct p.
-do 2 rewrite plus_0_n; assumption.
-intros x IH. do 2 rewrite plus_Sn_m. now apply <- lt_resp_S.
+do 2 rewrite plus_0_l; assumption.
+intros x IH. do 2 rewrite plus_S_l. now apply <- lt_resp_S.
 Qed.
 
-Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
+Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
 Proof.
 intros n m p H; rewrite plus_comm.
 set (k := p + n); rewrite plus_comm; unfold k; clear k.
 now apply plus_lt_compat_l.
 Qed.
 
-Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply lt_trans with (m := m + p);
 [now apply plus_lt_compat_r | now apply plus_lt_compat_l].
 Qed.
 
-Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
+Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m.
 Proof.
-intros n m p; induct p.
-now do 2 rewrite plus_0_n.
-intros x IH H.
-do 2 rewrite plus_Sn_m in H.
-apply IH; now apply -> lt_resp_S.
+intros p n m; induct p.
+now do 2 rewrite plus_0_l.
+intros p IH.
+do 2 rewrite plus_S_l. now rewrite lt_resp_S.
+Qed.
+
+Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m.
+Proof.
+intros p n m;
+setoid_replace (n + p) with (p + n) by apply plus_comm;
+setoid_replace (m + p) with (p + m) by apply plus_comm;
+apply plus_lt_cancel_l.
+Qed.
+
+(* The following property is similar to plus_repl_pair in NPlus.v
+and is used to prove the correctness of the definition of order
+on integers constructed from pairs of natural numbers *)
+
+Theorem plus_lt_repl_pair : forall n m n' m' u v,
+  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
+Proof.
+intros n m n' m' u v H1 H2.
+apply <- (plus_lt_cancel_r (n + m')) in H1.
+set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k.
+rewrite <- plus_assoc in H1.
+setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm.
+rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1.
+rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm.
+rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1.
+now rewrite plus_comm in H1.
+Qed.
+
+Theorem plus_gt_S :
+  forall n m p, n + m > S p -> (exists n', n == S n') \/ (exists m', m == S m').
+Proof.
+intros n m p H. apply lt_exists_pred in H. destruct H as [q H].
+now apply plus_eq_S in H.
 Qed.
 
 End NPlusOrderProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index ed3498f1c..1d1644891 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -1,4 +1,6 @@
-Require Import Ring.
+Require Export Ring.
+(* Since we define a ring here, it should be possible to call the tactic
+ring in the modules that use this module. Hence Export, not Import. *)
 Require Export NPlus.
 
 Module Type NTimesSignature.
@@ -11,101 +13,108 @@ Notation "x * y" := (times x y) : NatScope.
 
 Add Morphism times with signature E ==> E ==> E as times_wd.
 
-Axiom times_0_n : forall n, 0 * n == 0.
-Axiom times_Sn_m : forall n m, (S n) * m == m + n * m.
+Axiom times_0_r : forall n, n * 0 == 0.
+Axiom times_S_r : forall n m, n * (S m) == n * m + n.
+
+(* Here recursion is done on the second argument to conform to the
+usual definition of ordinal multiplication in set theory, which is not
+commutative. It seems, however, that this definition in set theory is
+unfortunate for two reasons. First, multiplication A * B of two ordinals A
+and B can be defined as (an order type of) the cartesian product B x A
+(not A x B) ordered lexicographically. For example, omega * 2 =
+2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...},
+while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) <
+(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in
+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 NTimesSignature.
 
 Module NTimesProperties (Import NTimesModule : NTimesSignature).
-Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.NatModule NPlusModule.
 Open Local Scope NatScope.
 
-Theorem mult_0_r : forall n, n * 0 == 0.
+Theorem times_0_l : forall n, 0 * n == 0.
 Proof.
 induct n.
-now rewrite times_0_n.
+now rewrite times_0_r.
 intros x IH.
-rewrite times_Sn_m; now rewrite plus_0_n.
+rewrite times_S_r. now rewrite plus_0_r.
 Qed.
 
-Theorem mult_0_l : forall n, 0 * n == 0.
+Theorem times_S_l : forall n m, (S n) * m == n * m + m.
 Proof.
-intro n; now rewrite times_0_n.
+intros n m; induct m.
+do 2 rewrite times_0_r; now rewrite plus_0_l.
+intros m IH. do 2 rewrite times_S_r. rewrite IH.
+do 2 rewrite <- plus_assoc. repeat rewrite plus_S_r.
+now setoid_replace (m + n) with (n + m); [| apply plus_comm].
 Qed.
 
-Theorem mult_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p.
+Theorem times_comm : forall n m, n * m == m * n.
 Proof.
-intros n m p; induct n.
-rewrite mult_0_l.
-now do 2 rewrite plus_0_l.
-intros x IH.
-rewrite plus_Sn_m.
-do 2 rewrite times_Sn_m.
-rewrite IH.
-apply plus_assoc.
+intros n m. induct n.
+rewrite times_0_l; now rewrite times_0_r.
+intros n IH. rewrite times_S_l; rewrite times_S_r. now rewrite IH.
 Qed.
 
-Theorem mult_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p.
+Theorem times_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p.
 Proof.
 intros n m p; induct n.
-do 3 rewrite mult_0_l; now rewrite plus_0_l.
-intros x IH.
-do 3 rewrite times_Sn_m.
-rewrite IH.
-(* Now we have to rearrange the sum of 4 terms *)
-rewrite <- (plus_assoc m p (x * m + x * p)).
-rewrite (plus_assoc p (x * m) (x * p)).
-rewrite (plus_comm p (x * m)).
-rewrite <- (plus_assoc (x * m) p (x * p)).
-apply (plus_assoc m (x * m) (p + x * p)).
+rewrite times_0_l. now do 2 rewrite plus_0_l.
+intros n IH. rewrite plus_S_l. do 2 rewrite times_S_l. rewrite IH.
+do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. apply plus_comm.
+Qed.
+
+Theorem times_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p.
+Proof.
+intros n m p.
+setoid_replace (n * (m + p)) with ((m + p) * n); [| apply times_comm].
+rewrite times_plus_distr_r.
+setoid_replace (n * m) with (m * n); [| apply times_comm].
+now setoid_replace (n * p) with (p * n); [| apply times_comm].
 Qed.
 
-Theorem mult_assoc : forall n m p, n * (m * p) == (n * m) * p.
+Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
 Proof.
 intros n m p; induct n.
-now do 3 rewrite mult_0_l.
-intros x IH.
-do 2 rewrite times_Sn_m.
-rewrite mult_plus_distr_r.
-now rewrite IH.
+now repeat rewrite times_0_l.
+intros n IH. do 2 rewrite times_S_l. rewrite IH. now rewrite times_plus_distr_r.
 Qed.
 
-Theorem mult_1_l : forall n, 1 * n == n.
+Theorem times_1_l : forall n, 1 * n == n.
 Proof.
-intro n.
-rewrite times_Sn_m; rewrite times_0_n. now rewrite plus_0_r.
+intro n. rewrite times_S_l; rewrite times_0_l. now rewrite plus_0_l.
 Qed.
 
-Theorem mult_1_r : forall n, n * 1 == n.
+Theorem times_1_r : forall n, n * 1 == n.
 Proof.
-induct n.
-now rewrite times_0_n.
-intros x IH.
-rewrite times_Sn_m; rewrite IH; rewrite plus_Sn_m; now rewrite plus_0_n.
+intro n; rewrite times_comm; apply times_1_l.
 Qed.
 
-Theorem mult_comm : forall n m, n * m == m * n.
+Lemma semi_ring : semi_ring_theory 0 (S 0) plus times E.
 Proof.
-intros n m.
-induct n.
-rewrite mult_0_l; now rewrite mult_0_r.
-intros x IH.
-rewrite times_Sn_m.
-assert (H : S x == S 0 + x).
-rewrite plus_Sn_m; rewrite plus_0_n; reflexivity.
-rewrite H.
-rewrite mult_plus_distr_l.
-rewrite mult_1_r; rewrite IH; reflexivity.
+constructor.
+exact plus_0_l.
+exact plus_comm.
+exact plus_assoc.
+exact times_1_l.
+exact times_0_l.
+exact times_comm.
+exact times_assoc.
+exact times_plus_distr_r.
 Qed.
 
+Add Ring SR : semi_ring.
+
 Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0.
 Proof.
 induct n; induct m.
 intros; now left.
 intros; now left.
 intros; now right.
-intros m IH H1.
-rewrite times_Sn_m in H1; rewrite plus_Sn_m in H1; now apply S_0 in H1.
+intros m IH H1. rewrite times_S_l in H1. rewrite plus_S_r in H1. now apply S_0 in H1.
 Qed.
 
 Definition times_eq_0_dec (n m : N) : bool :=
@@ -144,7 +153,7 @@ intro n; rewrite recursion_0; split; now intros.
 intro; rewrite recursion_0; rewrite (recursion_S eq_bool);
 [split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros].
 intro m; rewrite (recursion_S eq_bool).
-rewrite times_Sn_m. rewrite plus_Sn_m. intro H; now apply S_0 in H.
+rewrite times_S_l. rewrite plus_S_r. intro H; now apply S_0 in H.
 now unfold eq_bool.
 unfold fun2_wd; intros; now unfold eq_bool.
 Qed.
@@ -152,51 +161,44 @@ Qed.
 Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1.
 Proof.
 nondep_induct n; nondep_induct m.
-intro H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
-intros n H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
-intro H; rewrite mult_0_r in H; symmetry in H; now apply S_0 in H.
-intros m H; rewrite times_Sn_m in H; rewrite plus_Sn_m in H;
-apply S_inj in H; rewrite mult_comm in H; rewrite times_Sn_m in H;
-apply plus_eq_0 in H; destruct H as [H1 H2];
-apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split.
+intro H; rewrite times_0_l in H; symmetry in H; now apply S_0 in H.
+intros n H; rewrite times_0_l in H; symmetry in H; now apply S_0 in H.
+intro H; rewrite times_0_r in H; symmetry in H; now apply S_0 in H.
+intros m H; rewrite times_S_l in H; rewrite plus_S_r in H;
+apply S_inj in H; rewrite times_comm in H; rewrite times_S_l in H;
+apply plus_eq_0 in H; destruct H as [H1 H2].
+apply plus_eq_0 in H1; destruct H1 as [_ H3]; rewrite H2; rewrite H3; now split.
 Qed.
 
-(* See the notes on the theorem plus_repl_pair in NPlus.v *)
+(* In proving the correctness of the definition of multiplication on
+integers constructed from pairs of natural numbers, we'll need the
+following fact about natural numbers:
 
-Theorem plus_mult_repl_pair : forall a n m n' m' u v,
-  a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
-Proof.
-induct a.
-intros; repeat rewrite times_0_n in *; now repeat rewrite plus_0_n in *.
-intros a IH n m n' m' u v H1 H2.
-repeat rewrite times_Sn_m in *.
-(*setoid_replace (n + a * n) with (a * n + n) in H1 by (apply plus_comm).
-setoid_replace (m + a * m) with (a * m + m) in H1 by (apply plus_comm).*)
-setoid_replace (n' + a * n') with (a * n' + n') by (apply plus_comm).
-setoid_replace (m' + a * m') with (a * m' + m') by (apply plus_comm).
-do 2 rewrite <- plus_assoc. apply IH with n m; [| assumption]. do 2 rewrite plus_assoc.
-setoid_replace ((a * n) + n') with (n' + a * n) by (apply plus_comm).
-setoid_replace (a * m + m') with (m' + a * m) by (apply plus_comm).
-do 2 rewrite <- plus_assoc. apply plus_repl_pair with n m; [| assumption].
-now do 2 rewrite plus_assoc.
-Qed.
+a * x + u == a * y + v -> x + y' == x' + y -> a * x' + u = a * y' + v  (2)
+
+Here x + y' == x' + y represents equality of integers (x, y) and
+(x', y'), since a pair of natural numbers represents their integer
+difference. On integers, the (2) could be proved by moving
+a * y to the left, factoring out a and replacing x - y by x' - y'.
+However, the whole point is that we are only in the process of
+constructing integers, so this has to be proved for natural numbers,
+where we cannot move terms from one side of an equation to the other.
+This can be proved using the cancellation law plus_cancel_l. *)
 
-Theorem semi_ring : semi_ring_theory 0 (S 0) plus times E.
+Theorem plus_times_repl_pair : forall a n m n' m' u v,
+  a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
-constructor.
-exact plus_0_l.
-exact plus_comm.
-exact plus_assoc.
-exact mult_1_l.
-exact mult_0_l.
-exact mult_comm.
-exact mult_assoc.
-exact mult_plus_distr_r.
+intros a n m n' m' u v H1 H2.
+apply (times_wd a a) in H2; [| reflexivity].
+do 2 rewrite times_plus_distr_l in H2.
+symmetry in H2; add_equations H1 H2 as H3.
+stepl (a * n + (u + a * n' + a * m)) in H3 by ring.
+stepr (a * n + (a * m + v + a * m')) in H3 by ring.
+apply plus_cancel_l in H3.
+stepl (a * m + (u + a * n')) in H3 by ring.
+stepr (a * m + (v + a * m')) in H3 by ring.
+apply plus_cancel_l in H3.
+stepl (u + a * n') by ring. now stepr (v + a * m') by ring.
 Qed.
 
-Add Ring SR : semi_ring.
-Goal forall x y z : N, (x + y) * z == z * y + x * z.
-intros. Set Printing All. ring.
-
-
 End NTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimesOrder.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v
index 89ddcc7d4..ea189c60f 100644
--- a/theories/Numbers/Natural/Axioms/NTimesOrder.v
+++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v
@@ -9,55 +9,55 @@ Module Export NPlusOrderPropertiesModule :=
   NPlusOrderProperties NTimesModule.NPlusModule NOrderModule.
 Open Local Scope NatScope.
 
-Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Lemma times_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 Proof.
 intros n m p; induct n.
-now do 2 rewrite mult_1_l.
+now do 2 rewrite times_1_l.
 intros x IH H.
-rewrite times_Sn_m.
-set (k := S x * m); rewrite times_Sn_m; unfold k; clear k.
-apply plus_lt_compat; [assumption | apply IH; assumption].
+rewrite times_S_l.
+set (k := S x * m); rewrite times_S_l; unfold k; clear k.
+apply plus_lt_compat; [apply IH; assumption | assumption].
 Qed.
 
-Lemma mult_S_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n).
+Lemma times_S_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n).
 Proof.
 intros n m p H.
-set (k := (p * (S n))); rewrite mult_comm; unfold k; clear k.
-set (k := ((S n) * m)); rewrite mult_comm; unfold k; clear k.
-now apply mult_S_lt_compat_l.
+set (k := (p * (S n))); rewrite times_comm; unfold k; clear k.
+set (k := ((S n) * m)); rewrite times_comm; unfold k; clear k.
+now apply times_S_lt_compat_l.
 Qed.
 
-Lemma mult_lt_compat_l : forall m n p, n < m -> 0 < p -> p * n < p * m.
+Lemma times_lt_compat_l : forall m n p, n < m -> 0 < p -> p * n < p * m.
 Proof.
 intros n m p H1 H2.
 apply (lt_exists_pred p) in H2.
 destruct H2 as [q H]. repeat rewrite H.
-now apply mult_S_lt_compat_l.
+now apply times_S_lt_compat_l.
 Qed.
 
-Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
+Lemma times_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
 Proof.
 intros n m p H1 H2.
 apply (lt_exists_pred p) in H2.
 destruct H2 as [q H]. repeat rewrite H.
-now apply mult_S_lt_compat_r.
+now apply times_S_lt_compat_r.
 Qed.
 
-Lemma mult_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m.
+Lemma times_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (times_0_n m); now apply mult_lt_compat_r.
+rewrite <- (times_0_l m); now apply times_lt_compat_r.
 Qed.
 
-Lemma mult_lt_compat : forall n m p q, n < m -> p < q -> n * p < m * q.
+Lemma times_lt_compat : forall n m p q, n < m -> p < q -> n * p < m * q.
 Proof.
 intros n m p q; induct n.
-intros; rewrite times_0_n; apply mult_positive;
+intros; rewrite times_0_l; apply times_positive;
 [assumption | apply lt_positive with (n := p); assumption].
 intros x IH H1 H2.
 apply lt_trans with (m := ((S x) * q)).
-now apply mult_S_lt_compat_l; assumption.
-now apply mult_lt_compat_r; [| apply lt_positive with (n := p)].
+now apply times_S_lt_compat_l; assumption.
+now apply times_lt_compat_r; [| apply lt_positive with (n := p)].
 Qed.
 
 End NTimesOrderProperties.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index f87baf687..956c8b28c 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -124,12 +124,12 @@ Proof.
 unfold E; congruence.
 Qed.
 
-Theorem plus_0_n : forall n, 0 + n = n.
+Theorem plus_0_l : forall n, 0 + n = n.
 Proof.
 exact Nplus_0_l.
 Qed.
 
-Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m).
+Theorem plus_S_l : forall n m, (S n) + m = S (n + m).
 Proof.
 exact Nplus_succ.
 Qed.
@@ -146,46 +146,63 @@ Proof.
 unfold E; congruence.
 Qed.
 
-Theorem times_0_n : forall n, 0 * n = 0.
+Theorem times_0_r : forall n, n * 0 = 0.
 Proof.
-exact Nmult_0_l.
+intro n; rewrite Nmult_comm; apply Nmult_0_l.
 Qed.
 
-Theorem times_Sn_m : forall n m, (S n) * m = m + n * m.
+Theorem times_S_r : forall n m, n * (S m) = n * m + n.
 Proof.
-exact Nmult_Sn_m.
+intros n m; rewrite Nmult_comm; rewrite Nmult_Sn_m.
+rewrite Nplus_comm; now rewrite Nmult_comm.
 Qed.
 
 End NBinaryTimes.
 
-Module NBinaryLt <: NLtSignature.
+Module NBinaryOrder <: NOrderSignature.
 Module Export NatModule := BinaryNat.
 
-Definition lt (m n : N) := less_than (Ncompare m n).
+Definition lt (m n : N) := comp_bool (Ncompare m n) Lt.
+Definition le (m n : N) := let c := (Ncompare m n) in orb (comp_bool c Lt) (comp_bool c Eq).
 
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Proof.
 unfold E; congruence.
 Qed.
 
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
+Proof.
+intros n m.
+assert (H : (n ?= m) = Eq <-> n = m).
+(split; intro H); [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl].
+unfold le, lt; rewrite eq_true_or. repeat rewrite comp_bool_correct. now rewrite H.
+Qed.
+
 Theorem lt_0 : forall x, ~ (lt x 0).
 Proof.
 unfold lt; destruct x as [|x]; simpl; now intro.
 Qed.
 
-Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y.
+Theorem lt_S : forall x y, lt x (S y) <-> le x y.
 Proof.
-intros x y.
+intros x y. rewrite le_lt.
 assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt);
-[unfold lt, less_than; destruct (x ?= S y); simpl; split; now intro |].
+[unfold lt, comp_bool; destruct (x ?= S y); simpl; split; now intro |].
 assert (H2 : lt x y <-> Ncompare x y = Lt);
-[unfold lt, less_than; destruct (x ?= y); simpl; split; now intro |].
+[unfold lt, comp_bool; destruct (x ?= y); simpl; split; now intro |].
 pose proof (Ncompare_n_Sm x y) as H. tauto.
 Qed.
 
-End NBinaryLt.
+End NBinaryOrder.
+
+Module Export NBinaryTimesOrderProperties := NTimesOrderProperties NBinaryTimes NBinaryOrder.
 
-Module Export NBinaryTimesLtProperties := NTimesLtProperties NBinaryTimes NBinaryLt.
+(* Todo: N implements NPred.v and NMinus.v *)
 
 (*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0e07cd260..c1fc14a8a 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,26 +1,74 @@
 Require Import Minus.
 
+Require Export NPlus.
 Require Export NDepRec.
 Require Export NTimesOrder.
 Require Export NMinus.
 Require Export NMiscFunct.
 
-Module NPeanoDomain <: NDomainEqSignature.
-(*  with Definition N := nat
-  with Definition E := (@eq nat)
-  with Definition e := eq_nat_bool.*)
+(* First we define the functions that will be suppled as
+implementations. The parameters in module types, to which these
+functions are going to be assigned, are declared Inline,
+so in the properties functors the definitions are going to
+be unfolded and the theorems proved in these functors
+will contain these functions in their statements. *)
+
+(* Decidable equality *)
+Fixpoint e (x y : nat) {struct x} : bool :=
+match x, y with
+| 0, 0 => true
+| S x', S y' => e x' y'
+| _, _ => false
+end.
+
+(* The boolean < function can be defined as follows using the
+standard library:
+
+fun n m => proj1_sig (nat_lt_ge_bool n m)
+
+However, this definition seems too complex. First, there are many
+functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
+using bool_of_sumbool and
+
+lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
+
+where the latter function is defined using sumbool_not and
+
+le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
+
+Second, this definition is not the most efficient, especially since
+le_lt_dec is proved using tactics, not by giving the explicit proof
+term. *)
+
+Fixpoint lt (n m : nat) {struct n} : bool :=
+match n, m with
+| _, 0 => false
+| 0, S _ => true
+| S n', S m' => lt n' m'
+end.
+
+Fixpoint le (n m : nat) {struct n} : bool :=
+match n, m with
+| 0, _ => true
+| S n', S m' => le n' m'
+| S _, 0 => false
+end.
 
 Delimit Scope NatScope with Nat.
+Open Scope NatScope.
+
+(* Domain *)
+
+Module Export NPeanoDomain <: NDomainEqSignature.
 
 Definition N := nat.
 Definition E := (@eq nat).
-Definition e := eq_nat_bool.
+Definition e := e.
 
 Theorem E_equiv_e : forall x y : N, E x y <-> e x y.
 Proof.
-unfold E, e; intros x y; split; intro H;
-[rewrite H; apply eq_nat_bool_refl |
-now apply eq_nat_bool_implies_eq].
+induction x; destruct y; simpl; try now split; intro.
+rewrite <- IHx; split; intro H; [now injection H | now rewrite H].
 Qed.
 
 Definition E_equiv : equiv N E := eq_equiv N.
@@ -33,8 +81,8 @@ as E_rel.
 
 End NPeanoDomain.
 
-Module PeanoNat <: NatSignature.
-Module Export NDomainModule := NPeanoDomain.
+Module Export PeanoNat <: NatSignature.
+Module (*Import*) NDomainModule := NPeanoDomain.
 
 Definition O := 0.
 Definition S := S.
@@ -85,10 +133,9 @@ Qed.
 
 End PeanoNat.
 
-Module NPeanoDepRec <: NDepRecSignature.
-
-Module Export NDomainModule := NPeanoDomain.
-Module Export NatModule <: NatSignature := PeanoNat.
+Module Export NPeanoDepRec <: NDepRecSignature.
+Module Import NDomainModule := NPeanoDomain.
+Module Import NatModule := PeanoNat.
 
 Definition dep_recursion := nat_rec.
 
@@ -108,84 +155,102 @@ Qed.
 
 End NPeanoDepRec.
 
-Module NPeanoPlus <: NPlusSignature.
-Module Export NatModule := PeanoNat.
+Module Export NPeanoOrder <: NOrderSignature.
+Module Import NatModule := PeanoNat.
 
-Definition plus := plus.
+Definition lt := lt.
+Definition le := le.
 
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Proof.
-unfold E; congruence.
+unfold E, eq_bool; congruence.
 Qed.
 
-Theorem plus_0_n : forall n, 0 + n = n.
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
 Proof.
-reflexivity.
+unfold E, eq_bool; congruence.
 Qed.
 
-Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m).
+(* It would be easier to prove the boolean lemma first because
+|| is simplified by simpl unlike \/ *)
+Lemma le_lt_bool : forall x y, le x y = (lt x y) || (e x y).
 Proof.
-reflexivity.
+induction x as [| x IH]; destruct y; simpl; (reflexivity || apply IH).
 Qed.
 
-End NPeanoPlus.
-
-Module NPeanoTimes <: NTimesSignature.
-Module Export NPlusModule := NPeanoPlus.
-
-Definition times := mult.
+Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y.
+Proof.
+intros; rewrite E_equiv_e; rewrite <- eq_true_or;
+rewrite <- eq_true_iff; apply le_lt_bool.
+Qed.
 
-Add Morphism times with signature E ==> E ==> E as times_wd.
+Theorem lt_0 : forall x, ~ (lt x 0).
 Proof.
-unfold E; congruence.
+destruct x as [|x]; simpl; now intro.
 Qed.
 
-Theorem times_0_n : forall n, 0 * n = 0.
+Lemma lt_S_bool : forall x y, lt x (S y) = le x y.
 Proof.
-auto.
+unfold lt, le; induction x as [| x IH]; destruct y as [| y];
+simpl; try reflexivity.
+destruct x; now simpl.
+apply IH.
 Qed.
 
-Theorem times_Sn_m : forall n m, (S n) * m = m + n * m.
+Theorem lt_S : forall x y, lt x (S y) <-> le x y.
 Proof.
-auto.
+intros; rewrite <- eq_true_iff; apply lt_S_bool.
 Qed.
 
-End NPeanoTimes.
+End NPeanoOrder.
 
-Module NPeanoOrder <: NOrderSignature.
-Module Export NatModule := PeanoNat.
+Module Export NPeanoPlus <: NPlusSignature.
+Module (*Import*) NatModule := PeanoNat.
 
-Definition lt := lt_bool.
-Definition le := le_bool.
+Definition plus := plus.
 
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Notation "x + y" := (plus x y) : NatScope.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
 Proof.
-unfold E, eq_bool; congruence.
+unfold E; congruence.
 Qed.
 
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Theorem plus_0_l : forall n, 0 + n = n.
 Proof.
-unfold E, eq_bool; congruence.
+reflexivity.
 Qed.
 
-Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y.
+Theorem plus_S_l : forall n m, (S n) + m = S (n + m).
 Proof.
-exact le_lt.
+reflexivity.
 Qed.
 
-Theorem lt_0 : forall x, ~ (lt x 0).
+End NPeanoPlus.
+
+Module Export NPeanoTimes <: NTimesSignature.
+Module Import NPlusModule := NPeanoPlus.
+
+Definition times := mult.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
 Proof.
-exact lt_bool_0.
+unfold E; congruence.
 Qed.
 
-Theorem lt_S : forall x y, lt x (S y) <-> le x y.
+Theorem times_0_r : forall n, n * 0 = 0.
 Proof.
-exact lt_bool_S.
+auto.
 Qed.
 
-End NPeanoOrder.
+Theorem times_S_r : forall n m, n * (S m) = n * m + n.
+Proof.
+auto.
+Qed.
 
-Module NPeanoPred <: NPredSignature.
+End NPeanoTimes.
+
+Module Export NPeanoPred <: NPredSignature.
 Module Export NatModule := PeanoNat.
 
 Definition P (n : nat) :=
@@ -211,8 +276,8 @@ Qed.
 
 End NPeanoPred.
 
-Module NPeanoMinus <: NMinusSignature.
-Module Export NPredModule := NPeanoPred.
+Module Export NPeanoMinus <: NMinusSignature.
+Module Import NPredModule := NPeanoPred.
 
 Definition minus := minus.
 
@@ -245,3 +310,13 @@ Module Export NPeanoMinusProperties :=
 
 Module MiscFunctModule := MiscFunctFunctor PeanoNat.
 (* The instruction above adds about 0.5M to the size of the .vo file !!! *)
+
+(*Lemma e_implies_E : forall n m, e n m = true -> n = m.
+Proof.
+intros n m H; rewrite <- eq_true_unfold_pos in H;
+now apply <- E_equiv_e.
+Qed.
+
+Add Ring SR : semi_ring (decidable e_implies_E).
+
+Goal forall x y : nat, x + y = y + x. intros. ring.*)
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index b339fccf7..c59690887 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -1,14 +1,19 @@
 Require Export Setoid.
-Require Import Bool.
+Require Export Bool.
+(* Standard library. Export, not Import, because if a file
+importing the current file wants to use. e.g.,
+Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2,
+then it needs to know about bool and have a notation ||. *)
+
 
 (*
 Contents:
 - Coercion from bool to Prop
+- Extension of the tactics stepl and stepr
 - An attempt to extend setoid rewrite to formulas with quantifiers
 - Extentional properties of predicates, relations and functions
   (well-definedness and equality)
 - Relations on cartesian product
-- Some boolean functions on nat
 - Miscellaneous
 *)
 
@@ -19,18 +24,66 @@ Definition eq_bool := (@eq bool).
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 Coercion eq_true : bool >-> Sortclass.
 
-Theorem eq_true_unfold : forall b : bool, b <-> b = true.
+Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true.
 Proof.
-intro b; split; intro H.
-now inversion H.
-now rewrite H.
+intro b; split; intro H. now inversion H. now rewrite H.
+Qed.
+
+Theorem eq_true_unfold_neg : forall b : bool, ~ b <-> b = false.
+Proof.
+intros b; destruct b; simpl; rewrite eq_true_unfold_pos.
+split; intro H; [elim (H (refl_equal true)) | discriminate H].
+split; intro H; [reflexivity | discriminate].
+Qed.
+
+Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2.
+Proof.
+destruct b1; destruct b2; simpl; tauto.
+Qed.
+
+Theorem eq_true_and : forall b1 b2 : bool, b1 && b2 <-> b1 /\ b2.
+Proof.
+destruct b1; destruct b2; simpl; tauto.
+Qed.
+
+Theorem eq_true_neg : forall b : bool, negb b <-> ~ b.
+Proof.
+destruct b; simpl; rewrite eq_true_unfold_pos; rewrite eq_true_unfold_neg;
+split; now intro.
 Qed.
 
-Theorem eq_true_neg : forall x : bool, ~ x -> x = false.
+Theorem eq_true_iff : forall b1 b2 : bool, b1 = b2 <-> (b1 <-> b2).
 Proof.
-intros x H; destruct x; [elim (H is_eq_true) | reflexivity].
+intros b1 b2; split; intro H.
+now rewrite H.
+destruct b1; destruct b2; simpl; try reflexivity.
+apply -> eq_true_unfold_neg. rewrite H. now intro.
+symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro.
 Qed.
 
+(** Extension of the tactics stepl and stepr to make them
+applicable to hypotheses *)
+
+Tactic Notation "stepl" constr(t1') "in" hyp(H) :=
+match (type of H) with
+| ?R ?t1 ?t2 =>
+  let H1 := fresh in
+  cut (R t1' t2); [clear H; intro H | stepl t1; [assumption |]]
+| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
+end.
+
+Tactic Notation "stepl" constr(t1') "in" hyp(H) "by" tactic(r) := stepl t1' in H; [| r].
+
+Tactic Notation "stepr" constr(t2') "in" hyp(H) :=
+match (type of H) with
+| ?R ?t1 ?t2 =>
+  let H1 := fresh in
+  cut (R t1 t2'); [clear H; intro H | stepr t2; [assumption |]]
+| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
+end.
+
+Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].
+
 (** An attempt to extend setoid rewrite to formulas with quantifiers *)
 
 (* The following algorithm was explained to me by Bruno Barras.
@@ -252,100 +305,22 @@ End RelationOnProduct.
 Implicit Arguments prod_rel [A B].
 Implicit Arguments prod_rel_equiv [A B].
 
-(** Some boolean functions on nat. Their analogs are available in the
-standard library; however, we provide simpler definitions. Used in
-defining  implementations of natural numbers. *)
+(** Miscellaneous *)
 
-Fixpoint eq_nat_bool (x y : nat) {struct x} : bool :=
+Definition comp_bool (x y : comparison) : bool :=
 match x, y with
-| 0, 0 => true
-| S x', S y' => eq_nat_bool x' y'
-| _, _ => false
+| Lt, Lt => true
+| Eq, Eq => true
+| Gt, Gt => true
+| _, _   => false
 end.
 
-Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y -> x = y.
+Theorem comp_bool_correct : forall x y : comparison,
+  comp_bool x y <-> x = y.
 Proof.
-induction x; destruct y; simpl; intro H; try (reflexivity || inversion H).
-apply IHx in H; now rewrite H.
+destruct x; destruct y; simpl; split; now intro.
 Qed.
 
-Theorem eq_nat_bool_refl : forall x, eq_nat_bool x x.
-Proof.
-induction x; now simpl.
-Qed.
-
-Theorem eq_nat_correct : forall x y, eq_nat_bool x y <-> x = y.
-Proof.
-intros; split.
-now apply eq_nat_bool_implies_eq.
-intro H; rewrite H; apply eq_nat_bool_refl.
-Qed.
-
-(* The boolean less function can be defined as
-fun n m => proj1_sig (nat_lt_ge_bool n m)
-using the standard library.
-However, this definitionseems too complex. First, there are many
-functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
-using bool_of_sumbool and
-lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
-where the latter function is defined using sumbool_not and
-le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
-Second, this definition is not the most efficient, especially since
-le_lt_dec is proved using tactics, not by giving the explicit proof term. *)
-
-Fixpoint lt_bool (n m : nat) {struct n} : bool :=
-match n, m with
-| 0, S _ => true
-| S n', S m' => lt_bool n' m'
-| _, 0 => false
-end.
-
-Fixpoint le_bool (n m : nat) {struct n} : bool :=
-match n, m with
-| 0, _ => true
-| S n', S m' => le_bool n' m'
-| S _, 0 => false
-end.
-
-(* The following properties are used both in Peano.v and in MPeano.v *)
-
-Lemma le_lt_bool : forall x y, le_bool x y = (lt_bool x y) || (eq_nat_bool x y).
-Proof.
-induction x as [| x IH]; destruct y; simpl; (reflexivity || apply IH).
-Qed.
-
-Theorem le_lt : forall x y, le_bool x y <-> lt_bool x y \/ x = y.
-Proof.
-intros x y. rewrite le_lt_bool.
-setoid_replace (eq_true (lt_bool x y || eq_nat_bool x y)) with
-  (lt_bool x y = true \/ eq_nat_bool x y = true) using relation iff.
-do 2 rewrite <- eq_true_unfold. now rewrite eq_nat_correct.
-rewrite eq_true_unfold. split; [apply orb_prop | apply orb_true_intro].
-Qed. (* Can be simplified *)
-
-Theorem lt_bool_0 : forall x, ~ (lt_bool x 0).
-Proof.
-destruct x as [|x]; simpl; now intro.
-Qed.
-
-Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> le_bool x y.
-Proof.
-assert (A : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y).
-induction x as [| x IH]; destruct y as [| y]; simpl.
-split; [now right | now intro].
-split; [now left | now intro].
-split; [intro H; false_hyp H lt_bool_0 |
-intro H; destruct H as [H | H]; now auto].
-assert (H : x = y <-> S x = S y); [split; auto|].
-rewrite <- H; apply IH.
-intros; rewrite le_lt; apply A.
-Qed.
-
-(** Miscellaneous *)
-
-Definition less_than (x : comparison) : bool :=
-match x with Lt => true | _ => false end.
-
 Definition LE_Set : forall A : Set, relation A := (@eq).
 
 Lemma eq_equiv : forall A : Set, equiv A (LE_Set A).