An update on axiomatic number classes.

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

12 files changed, 498 insertions, 341 deletions

diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index da4c0af3d5..ceccf840a0 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 c525db3d21..de261bfbed 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 5b3fde2c23..52148cd384 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 1f112a7b44..70fd8c719f 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 12cecca18e..8743f5961f 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 08a6d44a85..1b631ce646 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 d49794d28d..3a7c19b62b 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 d152a03681..4119e3c248 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 ed3498f1c4..1d16448919 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 89ddcc7d44..ea189c60f7 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 f87baf687c..956c8b28c5 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 0e07cd260d..c1fc14a8ae 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.*)