An update on axiomatization of number classes.

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

17 files changed, 593 insertions, 347 deletions

diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index ad17e5255..da4c0af3d 100644
--- a/theories/Numbers/Natural/Axioms/NAxioms.v
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -5,21 +5,21 @@ Require Export NDomain.
 *********************************************************************)
 
 Module Type NatSignature.
-Declare Module Export DomainModule : DomainSignature.
+Declare Module Export NDomainModule : NDomainSignature.
 (* We use Export in the previous line to make sure that if we import a
 module of type NatSignature, then we also import (i.e., get access
-without path qualifiers to) DomainModule. For example, the functor
+without path qualifiers to) NDomainModule. For example, the functor
 NatProperties below, which accepts an implementation of NatSignature
 as an argument and imports it, will have access to N. Indeed, it does
 not make sense to get unqualified access to O and S but not to N. *)
 
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 Parameter Inline O : N.
 Parameter Inline S : N -> N.
 
-Notation "0" := O : NScope.
-Notation "1" := (S O) : NScope.
+Notation "0" := O : NatScope.
+Notation "1" := (S O) : NatScope.
 
 Add Morphism S with signature E ==> E as S_wd.
 
@@ -174,9 +174,56 @@ Implicit Arguments recursion_S [A].
 
 End NatSignature.
 
-Module NatProperties (Export NatModule : NatSignature).
-Module Export DomainPropertiesModule := DomainProperties DomainModule.
-Open Local Scope NScope.
+(* 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. *)
+
+Module Type NPredSignature.
+Declare Module Export NatModule : NatSignature.
+Open Local Scope NatScope.
+
+Parameter Inline P : N -> N.
+
+Add Morphism P with signature E ==> E as P_wd.
+
+Axiom P_0 : P 0 == 0.
+Axiom P_S : forall n, P (S n) == n.
+
+End NPredSignature.
+
+Module NDefPred (Import NM : NatSignature) <: NPredSignature.
+Module NatModule := NM.
+Open Local Scope NatScope.
+
+Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+intros; unfold P.
+now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |].
+Qed.
+
+Theorem P_0 : P 0 == 0.
+Proof.
+unfold P; now rewrite recursion_0.
+Qed.
+
+Theorem P_S : forall n, P (S n) == n.
+Proof.
+intro n; unfold P; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |].
+Qed.
+
+End NDefPred.
+
+Module NatProperties (Import NatModule : NatSignature).
+Module Export NDomainPropertiesModule := NDomainProperties NDomainModule.
+Module Import NDefPredModule := NDefPred NatModule. (* Many warnings are printed here !!! *)
+Open Local Scope NatScope.
 
 (* This tactic applies the induction axioms and solves the resulting
 goal "pred_wd E P" *)
@@ -223,30 +270,12 @@ change (LE_Set bool (if_zero false true (S n)) (if_zero false true 0)).
 rewrite H. unfold LE_Set. reflexivity.
 Qed.
 
-Definition pred (n : N) : N := recursion 0 (fun m _ => m) n.
-
-Add Morphism pred with signature E ==> E as pred_wd.
-Proof.
-intros; unfold pred.
-now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |].
-Qed.
-
-Theorem pred_0 : pred 0 == 0.
-Proof.
-unfold pred; now rewrite recursion_0.
-Qed.
-
-Theorem pred_S : forall n, pred (S n) == n.
-Proof.
-intro n; unfold pred; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |].
-Qed.
-
 Theorem S_inj : forall m n, S m == S n -> m == n.
 Proof.
 intros m n H.
-setoid_replace m with (pred (S m)) by (symmetry; apply pred_S).
-setoid_replace n with (pred (S n)) by (symmetry; apply pred_S).
-now apply pred_wd.
+setoid_replace m with (P (S m)) by (symmetry; apply P_S).
+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.
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
index 85ff0eb72..c525db3d2 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -5,13 +5,13 @@ equality. The reason is that, if the domain is A : nat -> Set, then (A
 n) must coincide with (A n') whenever n == n'. However, it is possible
 to try to use arbitrary domain and require that n == n' -> A n = A n'. *)
 
-Module Type DepRecSignature.
-Declare Module Export DomainModule : DomainEqSignature.
+Module Type NDepRecSignature.
+Declare Module Export NDomainModule : NDomainEqSignature.
 Declare Module Export NatModule : NatSignature with
-  Module DomainModule := DomainModule.
+  Module NDomainModule := NDomainModule.
 (* Instead of these two lines, I would like to say
-Declare Module Export Nat : NatSignature with Module Domain : NatEqDomain. *)
-Open Local Scope NScope.
+Declare Module Export Nat : NatSignature with Module NDomain : NatEqDomain. *)
+Open Local Scope NatScope.
 
 Parameter Inline dep_recursion :
   forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
@@ -24,14 +24,14 @@ Axiom dep_recursion_S :
   forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N),
     dep_recursion A a f (S n) = f n (dep_recursion A a f n).
 
-End DepRecSignature.
+End NDepRecSignature.
 
-Module DepRecTimesProperties
-  (Export DepRecModule : DepRecSignature)
-  (TimesModule : TimesSignature
-    with Module PlusModule.NatModule := DepRecModule.NatModule).
-Module Export TimesPropertiesModule := TimesProperties TimesModule.
-Open Local Scope NScope.
+Module NDepRecTimesProperties
+  (Import NDepRecModule : NDepRecSignature)
+  (Import NTimesModule : NTimesSignature
+    with Module NPlusModule.NatModule := NDepRecModule.NatModule).
+Module Export NTimesPropertiesModule := NTimesProperties NTimesModule.
+Open Local Scope NatScope.
 
 Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}.
 Proof.
@@ -68,4 +68,4 @@ intros n _ m _ H.
 rewrite times_Sn_m in H; rewrite plus_Sn_m in H; now apply S_0 in H.
 Qed.
 
-End DepRecTimesProperties.
+End NDepRecTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
index de2ddf116..5b3fde2c2 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -1,6 +1,6 @@
 Require Export NumPrelude.
 
-Module Type DomainSignature.
+Module Type NDomainSignature.
 
 Parameter Inline N : Set.
 Parameter Inline E : relation N.
@@ -28,17 +28,17 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Delimit Scope NScope with Nat.
-Bind Scope NScope with N.
-Notation "x == y" := (E x y) (at level 70) : NScope.
-Notation "x # y" := (~ E x y) (at level 70) : NScope.
+Delimit Scope NatScope with Nat.
+Bind Scope NatScope with N.
+Notation "x == y" := (E x y) (at level 70) : NatScope.
+Notation "x # y" := (~ E x y) (at level 70) : NatScope.
 
-End DomainSignature.
+End NDomainSignature.
 
-(* Now we give DomainSignature, but with E being Leibniz equality. If
+(* Now we give NDomainSignature, but with E being Leibniz equality. If
 an implementation uses this signature, then more facts may be proved
 about it. *)
-Module Type DomainEqSignature.
+Module Type NDomainEqSignature.
 
 Parameter Inline N : Set.
 Definition E := (@eq N).
@@ -53,17 +53,17 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-Delimit Scope NScope with Nat.
-Bind Scope NScope with N.
-Notation "x == y" := (E x y) (at level 70) : NScope.
-Notation "x # y" := ((E x y) -> False) (at level 70) : NScope.
+Delimit Scope NatScope with Nat.
+Bind Scope NatScope with N.
+Notation "x == y" := (E x y) (at level 70) : NatScope.
+Notation "x # y" := ((E x y) -> False) (at level 70) : NatScope.
 (* Why do we need a new notation for Leibniz equality? See DepRec.v *)
 
-End DomainEqSignature.
+End NDomainEqSignature.
 
-Module DomainProperties (Export DomainModule : DomainSignature).
+Module NDomainProperties (Import NDomainModule : NDomainSignature).
 (* It also accepts module of type NatDomainEq *)
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 (* The following easily follows from transitivity of e and E, but
 we need to deal with the coercion *)
@@ -79,4 +79,4 @@ assert (x == y); [rewrite Exx'; now rewrite Eyy' |
 rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
 Qed.
 
-End DomainProperties.
+End NDomainProperties.
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v
index 83bcf8ebe..ebd22e142 100644
--- a/theories/Numbers/Natural/Axioms/NIso.v
+++ b/theories/Numbers/Natural/Axioms/NIso.v
@@ -2,19 +2,15 @@ Require Export NAxioms.
 
 Module Homomorphism (Nat1 Nat2 : NatSignature).
 
-(*Module Import DomainProperties1 := DomainProperties Nat1.DomainModule.
-Module Import DomainProperties2 := DomainProperties Nat2.DomainModule.*)
-(* This registers Nat1.Domain.E and Nat2.Domain.E as setoid relations *)
-
-Notation Local N1 := Nat1.DomainModule.N.
-Notation Local N2 := Nat2.DomainModule.N.
-Notation Local E1 := Nat1.DomainModule.E.
-Notation Local E2 := Nat2.DomainModule.E.
+Notation Local N1 := Nat1.NDomainModule.N.
+Notation Local N2 := Nat2.NDomainModule.N.
+Notation Local E1 := Nat1.NDomainModule.E.
+Notation Local E2 := Nat2.NDomainModule.E.
 Notation Local O1 := Nat1.O.
 Notation Local O2 := Nat2.O.
 Notation Local S1 := Nat1.S.
 Notation Local S2 := Nat2.S.
-Notation Local "x == y" := (Nat2.DomainModule.E x y) (at level 70).
+Notation Local "x == y" := (Nat2.NDomainModule.E x y) (at level 70).
 
 Definition homomorphism (f : N1 -> N2) : Prop :=
   f O1 == O2 /\ forall x : N1, f (S1 x) == S2 (f x).
@@ -43,7 +39,7 @@ Theorem natural_isomorphism_S :
   forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x).
 Proof.
 unfold natural_isomorphism;
-intro x; now rewrite (Nat1.recursion_S Nat2.DomainModule.E);
+intro x; now rewrite (Nat1.recursion_S Nat2.NDomainModule.E);
 [| unfold fun2_wd; intros; apply Nat2.S_wd |].
 Qed.
 
@@ -64,12 +60,12 @@ NatProperties Nat1, it refers to Nat1.induction. *)
 Module Hom12 := Homomorphism Nat1 Nat2.
 Module Hom21 := Homomorphism Nat2 Nat1.
 
-Notation Local N1 := Nat1.DomainModule.N.
-Notation Local N2 := Nat2.DomainModule.N.
+Notation Local N1 := Nat1.NDomainModule.N.
+Notation Local N2 := Nat2.NDomainModule.N.
 Notation Local h12 := Hom12.natural_isomorphism.
 Notation Local h21 := Hom21.natural_isomorphism.
 
-Notation Local "x == y" := (Nat1.DomainModule.E x y) (at level 70).
+Notation Local "x == y" := (Nat1.NDomainModule.E x y) (at level 70).
 
 Lemma iso_inverse :
   forall x : N1, h21 (h12 x) == x.
@@ -91,10 +87,10 @@ Module Hom21 := Homomorphism Nat2 Nat1.
 Module Inverse121 := Inverse Nat1 Nat2.
 Module Inverse212 := Inverse Nat2 Nat1.
 
-Notation Local N1 := Nat1.DomainModule.N.
-Notation Local N2 := Nat2.DomainModule.N.
-Notation Local E1 := Nat1.DomainModule.E.
-Notation Local E2 := Nat2.DomainModule.E.
+Notation Local N1 := Nat1.NDomainModule.N.
+Notation Local N2 := Nat2.NDomainModule.N.
+Notation Local E1 := Nat1.NDomainModule.E.
+Notation Local E2 := Nat2.NDomainModule.E.
 Notation Local h12 := Hom12.natural_isomorphism.
 Notation Local h21 := Hom21.natural_isomorphism.
 
diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v
deleted file mode 100644
index 254db11d6..000000000
--- a/theories/Numbers/Natural/Axioms/NLt.v
+++ /dev/null
@@ -1,169 +0,0 @@
-Require Export NAxioms.
-
-Module Type LtSignature.
-Declare Module Export NatModule : NatSignature.
-Open Local Scope NScope.
-
-Parameter Inline lt : N -> N -> bool.
-
-Notation "x < y" := (lt x y) : NScope.
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-
-Axiom lt_0 : forall x, ~ (x < 0).
-Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y.
-End LtSignature.
-
-Module LtProperties (Export LtModule : LtSignature).
-Module Export NatPropertiesModule := NatProperties NatModule.
-Open Local Scope NScope.
-
-Theorem lt_n_Sn : forall n, n < S n.
-Proof.
-intro n. apply <- lt_S. now right.
-Qed.
-
-Theorem lt_closed_S : forall n m, n < m -> n < S m.
-Proof.
-intros. apply <- lt_S. now left.
-Qed.
-
-Theorem lt_S_lt : forall n m, S n < m -> n < m.
-Proof.
-intro n; induct m.
-intro H; absurd_hyp H; [apply lt_0 | assumption].
-intros x IH H.
-apply -> lt_S in H; elim H.
-intro H1; apply IH in H1; now apply lt_closed_S.
-intro H1; rewrite <- H1.
-apply lt_closed_S; apply lt_n_Sn.
-Qed.
-
-Theorem lt_0_Sn : forall n, 0 < S n.
-Proof.
-induct n; [apply lt_n_Sn | intros x H; now apply lt_closed_S].
-Qed.
-
-Theorem lt_transitive : forall n m p, n < m -> m < p -> n < p.
-Proof.
-intros n m p; induct m.
-intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption].
-intros x IH H1 H2.
-apply -> lt_S in H1; elim H1.
-intro H; apply IH; [assumption | apply lt_S_lt; assumption].
-intro H; rewrite H; apply lt_S_lt; assumption.
-Qed.
-
-Theorem lt_positive : forall n m, n < m -> 0 < m.
-Proof.
-intros n m; induct n.
-trivial.
-intros x IH H.
-apply lt_transitive with (m := S x); [apply lt_0_Sn | apply H].
-Qed.
-
-Theorem S_respects_lt : forall n m, S n < S m <-> n < m.
-Proof.
-intros n m; split.
-intro H; apply -> lt_S in H; elim H.
-intros; apply lt_S_lt; assumption.
-intro H1; rewrite <- H1; apply lt_n_Sn.
-induct m.
-intro H; absurd_hyp H; [ apply lt_0 | assumption].
-intros x IH H.
-apply -> lt_S in H; elim H; intro H1.
-apply lt_transitive with (m := S x).
-apply IH; assumption.
-apply lt_n_Sn.
-rewrite H1; apply lt_n_Sn.
-Qed.
-
-Theorem lt_n_m : forall n m, n < m <-> S n < m \/ S n == m.
-Proof.
-intros n m; nondep_induct m.
-split; intro H; [false_hyp H lt_0 |
-destruct H as [H | H]; [false_hyp H lt_0 | false_hyp H S_0]].
-intros m; split; intro H.
-apply -> lt_S in H. destruct H; [left; now apply <- S_respects_lt | right; now apply S_wd].
-destruct H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] |
-apply S_inj in H; rewrite H; apply lt_n_Sn].
-Qed.
-
-Theorem lt_irreflexive : forall n, ~ (n < n).
-Proof.
-induct n.
-apply lt_0.
-intro x; unfold not; intros H1 H2; apply H1; now apply -> S_respects_lt.
-Qed.
-
-Theorem neq_0_lt : forall n, 0 # n -> 0 < n.
-Proof.
-induct n.
-intro H; now elim H.
-intros; apply lt_0_Sn.
-Qed.
-
-Theorem lt_0_neq : forall n, 0 < n -> 0 # n.
-Proof.
-induct n.
-intro H; absurd_hyp H; [apply lt_0 | assumption].
-unfold not; intros; now apply S_0 with (n := n).
-Qed.
-
-Theorem lt_asymmetric : forall n m, ~ (n < m /\ m < n).
-Proof.
-unfold not; intros n m [H1 H2].
-now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|].
-Qed.
-
-Theorem eq_0_or_lt_0: forall n, 0 == n \/ 0 < n.
-Proof.
-induct n; [now left | intros x; right; apply lt_0_Sn].
-Qed.
-
-Theorem lt_options : forall n m, n < m -> S n < m \/ S n == m.
-Proof.
-intros n m; induct m.
-intro H; false_hyp H lt_0.
-intros x IH H.
-apply -> lt_S in H; elim H; intro H1.
-apply IH in H1; elim H1; intro H2.
-left; apply lt_transitive with (m := x); [assumption | apply lt_n_Sn].
-rewrite H2; left; apply lt_n_Sn.
-right; rewrite H1; reflexivity.
-Qed.
-
-Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n.
-Proof.
-intros n m; induct n.
-assert (H : 0 == m \/ 0 < m); [apply eq_0_or_lt_0 | tauto].
-intros n IH. destruct IH as [H | H].
-assert (S n < m \/ S n == m); [now apply lt_options | tauto].
-destruct H as [H1 | H1].
-right; right; rewrite H1; apply lt_n_Sn.
-right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn].
-Qed.
-
-Theorem lt_dichotomy : forall n m, n < m \/ ~ n < m.
-Proof.
-intros n m; pose proof (lt_trichotomy n m) as H.
-destruct H as [H1 | H1]; [now left |].
-destruct H1 as [H2 | H2].
-right; rewrite H2; apply lt_irreflexive.
-right; intro; apply (lt_asymmetric n m); split; assumption.
-Qed.
-
-Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n.
-Proof.
-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.
-Proof.
-induct n.
-intro H; false_hyp H lt_0.
-intros n IH H; now exists n.
-Qed.
-
-End LtProperties.
diff --git a/theories/Numbers/Natural/Axioms/NMinus.v b/theories/Numbers/Natural/Axioms/NMinus.v
new file mode 100644
index 000000000..1f112a7b4
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NMinus.v
@@ -0,0 +1,81 @@
+Require Export NPlusOrder.
+
+Module Type NMinusSignature.
+Declare Module Export NPredModule : NPredSignature.
+Open Local Scope NatScope.
+
+Parameter Inline minus : N -> N -> N.
+
+Notation "x - y" := (minus x y) : NatScope.
+
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+
+Axiom minus_0_r : forall n, n - 0 == n.
+Axiom minus_S_r : forall n m, n - (S m) == P (n - m).
+
+End NMinusSignature.
+
+Module NMinusProperties (Import NMinusModule : NMinusSignature)
+                        (Import NPlusModule : NPlusSignature with
+                          Module NatModule := NMinusModule.NPredModule.NatModule)
+                        (Import NOrderModule : NOrderSignature with
+                          Module NatModule := NMinusModule.NPredModule.NatModule).
+Module Export NPlusOrderPropertiesModule :=
+  NPlusOrderProperties NPlusModule NOrderModule.
+Open Local Scope NatScope.
+
+Theorem minus_1_r : forall n, n - 1 == P n.
+Proof.
+intro n; rewrite minus_S_r; now rewrite minus_0_r.
+Qed.
+
+Theorem minus_0_l : forall n, 0 - n == 0.
+Proof.
+induct n.
+apply minus_0_r.
+intros n IH; rewrite minus_S_r; rewrite IH. now apply P_0.
+Qed.
+
+Theorem minus_comm_S : forall n m, S n - S m == n - m.
+Proof.
+intro n; induct m.
+rewrite minus_S_r. do 2 rewrite minus_0_r. now rewrite P_S.
+intros m IH. rewrite minus_S_r. rewrite IH. now rewrite minus_S_r.
+Qed.
+
+Theorem minus_S_l : forall n m, n <= m -> S m - n == S (m - n).
+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.
+intros; now do 2 rewrite minus_0_r.
+clear n m H. intros n m H1 H2.
+now do 2 rewrite minus_comm_S. assumption.
+Qed.
+
+Theorem minus_le : forall n m, n <= m -> n - m == 0.
+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.
+apply minus_0_l.
+clear n m H; intros n m H1 H2. now rewrite minus_comm_S.
+assumption.
+Qed.
+
+Theorem minus_diag : forall n, n - n == 0.
+Proof.
+intro n; apply minus_le; apply le_refl.
+Qed.
+
+Theorem minus_plus : forall n m, n <= m -> (m - n) + n == m.
+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.
+now rewrite H2.
+assumption.
+Qed.
+
+End NMinusProperties.
+
+
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 38af96b1d..3b0c1c5eb 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -1,11 +1,10 @@
-Require Export Bool. (* To get the negb function *)
+Require Import Bool. (* To get the orb and negb function *)
 Require Export NStrongRec.
-Require Export NTimesLt.
+Require Export NTimesOrder.
 
-Module MiscFunctFunctor (NatMod : NatSignature).
-Module Export NatPropertiesModule := NatProperties NatMod.
+Module MiscFunctFunctor (Import NatMod : NatSignature).
 Module Export StrongRecPropertiesModule := StrongRecProperties NatMod.
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 (*****************************************************)
 (**                   Addition                       *)
@@ -84,6 +83,16 @@ Definition lt (m : N) : N -> bool :=
             (fun _ f => fun n => recursion false (fun n' _ => f n') n)
             m.
 
+(* It would be more efficient to make a three-way comparison, i.e.,
+return Eq, Lt, or Gt, but since these are no-use default functions,
+we define <= as (< or =) *)
+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 4 rewrite eq_true_unfold.
+
 Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true).
 unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_Set.
 Qed.
@@ -286,7 +295,7 @@ Qed.
 (** via recursion, we form the corresponding modules and *)
 (** apply the properties functors to these modules       *)
 
-Module DefaultPlusModule <: PlusSignature.
+Module NDefaultPlusModule <: NPlusSignature.
 
 Module NatModule := NatMod.
 (* If we used the name NatModule instead of NatMod then this would
@@ -310,10 +319,10 @@ Proof.
 exact plus_S.
 Qed.
 
-End DefaultPlusModule.
+End NDefaultPlusModule.
 
-Module DefaultTimesModule <: TimesSignature.
-Module PlusModule := DefaultPlusModule.
+Module NDefaultTimesModule <: NTimesSignature.
+Module NPlusModule := NDefaultPlusModule.
 
 Definition times := times.
 
@@ -332,9 +341,9 @@ Proof.
 exact times_S.
 Qed.
 
-End DefaultTimesModule.
+End NDefaultTimesModule.
 
-Module DefaultLtModule <: LtSignature.
+Module NDefaultOrderModule <: NOrderSignature.
 Module NatModule := NatMod.
 
 Definition lt := lt.
@@ -354,16 +363,9 @@ Proof.
 exact lt_S.
 Qed.
 
-End DefaultLtModule.
-
-Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule.
-Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule.
-Module Export DefaultLtProperties := LtProperties DefaultLtModule.
-Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
-Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
+End NDefaultOrderModule.
 
-(*Opaque MiscFunctFunctor.plus.
-Check plus_comm. (* This produces the following *)
-Eval compute in (forall n m : PlusModule.NatModule.DomainModule.N, plus n m == plus m n).*)
+Module Export DefaultTimesOrderProperties :=
+  NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule.
 
 End MiscFunctFunctor.
diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v
new file mode 100644
index 000000000..c4e9a21a7
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NOrder.v
@@ -0,0 +1,263 @@
+Require Export NAxioms.
+
+Module Type NOrderSignature.
+Declare Module Export NatModule : NatSignature.
+Open Local Scope NatScope.
+
+Parameter Inline lt : N -> N -> bool.
+Parameter Inline le : N -> N -> bool.
+
+Notation "x < y" := (lt x y) : NatScope.
+Notation "x <= y" := (le x y) : NatScope.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+
+Axiom le_lt : forall x y, x <= y <-> x < y \/ x == y.
+Axiom lt_0 : forall x, ~ (x < 0).
+Axiom lt_S : forall x y, x < S y <-> x <= y.
+End NOrderSignature.
+
+Module NOrderProperties (Import NOrderModule : NOrderSignature).
+Module Export NatPropertiesModule := NatProperties NatModule.
+Open Local Scope NatScope.
+
+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].
+
+Theorem le_refl : forall n, n <= n.
+Proof.
+intro; now le_intro2.
+Qed.
+
+Theorem le_0_r : forall n, n <= 0 -> n == 0.
+Proof.
+intros n H; le_elim H; [false_hyp H lt_0 | assumption].
+Qed.
+
+Theorem lt_n_Sn : forall n, n < S n.
+Proof.
+intro n. apply <- lt_S. now le_intro2.
+Qed.
+
+Theorem lt_closed_S : forall n m, n < m -> n < S m.
+Proof.
+intros. apply <- lt_S. now le_intro1.
+Qed.
+
+Theorem lt_S_lt : forall n m, S n < m -> n < m.
+Proof.
+intro n; induct m.
+intro H; absurd_hyp H; [apply lt_0 | assumption].
+intros x IH H.
+apply -> lt_S in H. le_elim H.
+apply IH in H; now apply lt_closed_S.
+rewrite <- H.
+apply lt_closed_S; apply lt_n_Sn.
+Qed.
+
+Theorem lt_0_Sn : forall n, 0 < S n.
+Proof.
+induct n; [apply lt_n_Sn | intros x H; now apply lt_closed_S].
+Qed.
+
+Theorem lt_transitive : forall n m p, n < m -> m < p -> n < p.
+Proof.
+intros n m p; induct m.
+intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption].
+intros x IH H1 H2.
+apply -> lt_S in H1. le_elim H1.
+apply IH; [assumption | apply lt_S_lt; assumption].
+rewrite H1; apply lt_S_lt; assumption.
+Qed.
+
+Theorem lt_positive : forall n m, n < m -> 0 < m.
+Proof.
+intros n m; induct n.
+trivial.
+intros x IH H.
+apply lt_transitive with (m := S x); [apply lt_0_Sn | apply H].
+Qed.
+
+Theorem lt_resp_S : forall n m, S n < S m <-> n < m.
+Proof.
+intros n m; split.
+intro H; apply -> lt_S in H; le_elim H.
+intros; apply lt_S_lt; assumption.
+rewrite <- H; apply lt_n_Sn.
+induct m.
+intro H; false_hyp H lt_0.
+intros x IH H.
+apply -> lt_S in H; le_elim H.
+apply lt_transitive with (m := S x).
+apply IH; assumption.
+apply lt_n_Sn.
+rewrite H; apply lt_n_Sn.
+Qed.
+
+Theorem le_resp_S : forall n m, S n <= S m <-> n <= m.
+Proof.
+intros n m; do 2 rewrite le_lt.
+pose proof (S_wd n m); pose proof (S_inj n m); pose proof (lt_resp_S n m); tauto.
+Qed.
+
+Theorem lt_le_S_l : forall n m, n < m <-> S n <= m.
+Proof.
+intros n m; nondep_induct m.
+split; intro H; [false_hyp H lt_0 |
+le_elim H; [false_hyp H lt_0 | false_hyp H S_0]].
+intros m; split; intro H.
+apply -> lt_S in H. le_elim H; [le_intro1; now apply <- lt_resp_S | le_intro2; now apply S_wd].
+le_elim H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] |
+apply S_inj in H; rewrite H; apply lt_n_Sn].
+Qed.
+
+Theorem le_S_0 : forall n, ~ (S n <= 0).
+Proof.
+intros n H; apply <- lt_le_S_l in H; false_hyp H lt_0.
+Qed.
+
+Theorem le_S_l_le : forall n m, S n <= m -> n <= m.
+Proof.
+intros; le_intro1; now apply <- lt_le_S_l.
+Qed.
+
+Theorem lt_irreflexive : forall n, ~ (n < n).
+Proof.
+induct n.
+apply lt_0.
+intro x; unfold not; intros H1 H2; apply H1; now apply -> lt_resp_S.
+Qed.
+
+Theorem neq_0_lt : forall n, 0 # n -> 0 < n.
+Proof.
+induct n.
+intro H; now elim H.
+intros; apply lt_0_Sn.
+Qed.
+
+Theorem lt_0_neq : forall n, 0 < n -> 0 # n.
+Proof.
+induct n.
+intro H; absurd_hyp H; [apply lt_0 | assumption].
+unfold not; intros; now apply S_0 with (n := n).
+Qed.
+
+Theorem lt_asymmetric : forall n m, ~ (n < m /\ m < n).
+Proof.
+unfold not; intros n m [H1 H2].
+now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|].
+Qed.
+
+Theorem le_0_l: forall n, 0 <= n.
+Proof.
+induct n; [now le_intro2 | intros; le_intro1; apply lt_0_Sn].
+Qed.
+
+Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n.
+Proof.
+intros n m; induct n.
+assert (H : 0 <= m); [apply le_0_l | apply -> le_lt in H; tauto].
+intros n IH. destruct IH as [H | H].
+assert (H1 : S n <= m); [now apply -> lt_le_S_l | apply -> le_lt in H1; tauto].
+destruct H as [H | H].
+right; right; rewrite H; apply lt_n_Sn.
+right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn].
+Qed.
+
+Theorem lt_dichotomy : forall n m, n < m \/ ~ n < m.
+Proof.
+intros n m; pose proof (lt_trichotomy n m) as H.
+destruct H as [H1 | H1]; [now left |].
+destruct H1 as [H2 | H2].
+right; rewrite H2; apply lt_irreflexive.
+right; intro; apply (lt_asymmetric n m); split; assumption.
+Qed.
+
+Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n.
+Proof.
+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.
+Proof.
+induct n.
+intro H; false_hyp H lt_0.
+intros n IH H; now exists n.
+Qed.
+
+(** Elimination principles for < and <= *)
+
+Section Induction1.
+
+Variable Q : N -> Prop.
+Hypothesis Q_wd : pred_wd E Q.
+Variable n : N.
+
+Add Morphism Q with signature E ==> iff as Q_morph1.
+Proof Q_wd.
+
+Theorem le_ind :
+  Q n ->
+  (forall m, n <= m -> Q m -> Q (S m)) ->
+  forall m, n <= m -> Q m.
+Proof.
+intros Base Step. induct m.
+intro H. apply le_0_r in H. now rewrite <- H.
+intros m IH H. le_elim H.
+apply -> lt_S in H. now apply Step; [| apply IH].
+now rewrite <- H.
+Qed.
+
+Theorem lt_ind :
+  Q (S n) ->
+  (forall m, n < m -> Q m -> Q (S m)) ->
+   forall m, n < m -> Q m.
+Proof.
+intros Base Step. induct m.
+intro H; false_hyp H lt_0.
+intros m IH H. apply -> lt_S in H. le_elim H.
+now apply Step; [| apply IH]. now rewrite <- H.
+Qed.
+
+End Induction1.
+
+Section Induction2.
+
+(* Variable Q : relation N. -- does not work !!! *)
+Variable Q : N -> N -> Prop.
+Hypothesis Q_wd : rel_wd E Q.
+
+Add Morphism Q with signature E ==> E ==> iff as Q_morph2.
+Proof Q_wd.
+
+Theorem le_ind_rel :
+   (forall m, Q 0 m) ->
+   (forall n m, n <= m -> Q n m -> Q (S n) (S m)) ->
+   forall n m, n <= m -> Q n m.
+Proof.
+intros Base Step; induct n.
+intros; apply Base.
+intros n IH m; nondep_induct m.
+intro H; false_hyp H le_S_0.
+intros m H. apply -> le_resp_S in H. now apply Step; [| apply IH].
+Qed.
+
+Theorem lt_ind_rel :
+   (forall m, Q 0 (S m)) ->
+   (forall n m, n < m -> Q n m -> Q (S n) (S m)) ->
+   forall n m, n < m -> Q n m.
+Proof.
+intros Base Step; induct n.
+intros m H. apply lt_exists_pred in H; destruct H as [m' H].
+rewrite H; apply Base.
+intros n IH m; nondep_induct m.
+intro H; false_hyp H lt_0.
+intros m H. apply -> lt_resp_S in H. now apply Step; [| apply IH].
+Qed.
+
+End Induction2.
+
+End NOrderProperties.
diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v
index 6f51330f3..cf6738750 100644
--- a/theories/Numbers/Natural/Axioms/NOtherInd.v
+++ b/theories/Numbers/Natural/Axioms/NOtherInd.v
@@ -1,6 +1,6 @@
 Require Export NDomain.
-Declare Module Export DomainModule : DomainSignature.
-Open Local Scope NScope.
+Declare Module Export NDomainModule : NDomainSignature.
+Open Local Scope NatScope.
 
 Parameter O : N.
 Parameter S : N -> N.
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index 63cc8a40f..0ae12df97 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -1,25 +1,23 @@
 Require Export NAxioms.
 
-Module Type PlusSignature.
+Module Type NPlusSignature.
 Declare Module Export NatModule : NatSignature.
-(* We use Export here because if we have an access to plus,
-then we need also an access to S and N *)
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 Parameter Inline plus : N -> N -> N.
 
-Notation "x + y" := (plus x y) : NScope.
+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).
 
-End PlusSignature.
+End NPlusSignature.
 
-Module PlusProperties (Export PlusModule : PlusSignature).
+Module NPlusProperties (Import NPlusModule : NPlusSignature).
 Module Export NatPropertiesModule := NatProperties NatModule.
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 Theorem plus_0_r : forall n, n + 0 == n.
 Proof.
@@ -199,4 +197,4 @@ rewrite plus_Sn_m in H. apply S_inj in H.
 apply plus_eq_0 in H; split; [apply S_wd | ]; tauto.
 Qed.
 
-End PlusProperties.
+End NPlusProperties.
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v
index 3724f9ec5..fe43ff38d 100644
--- a/theories/Numbers/Natural/Axioms/NPlusLt.v
+++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v
@@ -1,12 +1,12 @@
 Require Export NPlus.
-Require Export NLt.
+Require Export NOrder.
 
-Module PlusLtProperties (PlusModule : PlusSignature)
-                        (LtModule : LtSignature with
-                           Module NatModule := PlusModule.NatModule).
-Module Export PlusPropertiesModule := PlusProperties PlusModule.
-Module Export LtPropertiesModule := LtProperties LtModule.
-Open Local Scope NScope.
+Module NPlusOrderProperties (Import NPlusModule : NPlusSignature)
+                         (Import NOrderModule : NOrderSignature with
+                           Module NatModule := NPlusModule.NatModule).
+Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NOrderPropertiesModule := NOrderProperties NOrderModule.
+Open Local Scope NatScope.
 
 (* Print All locks up here !!! *)
 Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
@@ -21,7 +21,7 @@ Lemma 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 <- S_respects_lt.
+intros x IH. do 2 rewrite plus_Sn_m. now apply <- lt_resp_S.
 Qed.
 
 Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
@@ -44,7 +44,7 @@ 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 -> S_respects_lt.
+apply IH; now apply -> lt_resp_S.
 Qed.
 
-End PlusLtProperties.
+End NPlusOrderProperties.
diff --git a/theories/Numbers/Natural/Axioms/NPred.v b/theories/Numbers/Natural/Axioms/NPred.v
new file mode 100644
index 000000000..d3da22660
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NPred.v
@@ -0,0 +1,45 @@
+Require Export NAxioms.
+
+(* 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. *)
+
+Module Type NPredSignature.
+Declare Module Export NatModule : NatSignature.
+Open Local Scope NatScope.
+
+Parameter Inline P : N -> N.
+
+Add Morphism P with signature E ==> E as P_wd.
+
+Axiom P_0 : P 0 == 0.
+Axiom P_S : forall n, P (S n) == n.
+
+End NPredSignature.
+
+Module NDefPred (Import NM : NatSignature) <: NPredSignature.
+Module NatModule := NM.
+Open Local Scope NatScope.
+
+Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+intros; unfold P.
+now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |].
+Qed.
+
+Theorem P_0 : P 0 == 0.
+Proof.
+unfold P; now rewrite recursion_0.
+Qed.
+
+Theorem P_S : forall n, P (S n) == n.
+Proof.
+intro n; unfold P; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |].
+Qed.
+
+End NDefPred.
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v
index a2e73f99a..5c9a65781 100644
--- a/theories/Numbers/Natural/Axioms/NStrongRec.v
+++ b/theories/Numbers/Natural/Axioms/NStrongRec.v
@@ -1,8 +1,8 @@
 Require Export NAxioms.
 
-Module StrongRecProperties (NatModule : NatSignature).
+Module StrongRecProperties (Import NatModule : NatSignature).
 Module Export NatPropertiesModule := NatProperties NatModule.
-Open Local Scope NScope.
+Open Local Scope NatScope.
 
 Section StrongRecursion.
 
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index 4d1d2b0ca..2dd052201 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -1,23 +1,23 @@
 Require Export NPlus.
 
-Module Type TimesSignature.
-Declare Module Export PlusModule : PlusSignature.
-Open Local Scope NScope.
+Module Type NTimesSignature.
+Declare Module Export NPlusModule : NPlusSignature.
+Open Local Scope NatScope.
 
 Parameter Inline times : N -> N -> N.
 
-Notation "x * y" := (times x y) : NScope.
+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.
 
-End TimesSignature.
+End NTimesSignature.
 
-Module TimesProperties (Export TimesModule : TimesSignature).
-Module Export PlusPropertiesModule := PlusProperties PlusModule.
-Open Local Scope NScope.
+Module NTimesProperties (Import NTimesModule : NTimesSignature).
+Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Open Local Scope NatScope.
 
 Theorem mult_0_r : forall n, n * 0 == 0.
 Proof.
@@ -160,4 +160,4 @@ 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.
 Qed.
 
-End TimesProperties.
+End NTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v
index 36989f1b3..f6afd5999 100644
--- a/theories/Numbers/Natural/Axioms/NTimesLt.v
+++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v
@@ -1,14 +1,13 @@
 Require Export NTimes.
-Require Export NPlusLt.
+Require Export NPlusOrder.
 
-Module TimesLtProperties (TimesModule : TimesSignature)
-                         (LtModule : LtSignature with
-                            Module NatModule := TimesModule.PlusModule.NatModule).
-Module Export TimesPropertiesModule :=
-  TimesProperties TimesModule.
-Module Export PlusLtPropertiesModule :=
-  PlusLtProperties TimesModule.PlusModule LtModule.
-Open Local Scope NScope.
+Module NTimesOrderProperties (Import NTimesModule : NTimesSignature)
+                          (Import NOrderModule : NOrderSignature with
+                            Module NatModule := NTimesModule.NPlusModule.NatModule).
+Module Export NTimesPropertiesModule :=  NTimesProperties NTimesModule.
+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.
 Proof.
@@ -61,4 +60,4 @@ now apply mult_S_lt_compat_l; assumption.
 now apply mult_lt_compat_r; [| apply lt_positive with (n := p)].
 Qed.
 
-End TimesLtProperties.
+End NTimesOrderProperties.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 77fbdcaf7..f87baf687 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -2,12 +2,13 @@ Require Import NArith.
 Require Import Ndec.
 
 Require Export NDepRec.
-Require Export NTimesLt.
+Require Export NTimesOrder.
+Require Export NMinus.
 Require Export NMiscFunct.
 
 Open Local Scope N_scope.
 
-Module BinaryDomain : DomainEqSignature
+Module NBinaryDomain : NDomainEqSignature
   with Definition N := N
   with Definition E := (@eq N)
   with Definition e := Neqb.
@@ -31,11 +32,10 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-End BinaryDomain.
+End NBinaryDomain.
 
 Module BinaryNat <: NatSignature.
-
-Module Export DomainModule := BinaryDomain.
+Module Export NDomainModule := NBinaryDomain.
 
 Definition O := N0.
 Definition S := Nsucc.
@@ -92,8 +92,8 @@ Qed.
 
 End BinaryNat.
 
-Module BinaryDepRec <: DepRecSignature.
-Module Export DomainModule := BinaryDomain.
+Module NBinaryDepRec <: NDepRecSignature.
+Module Export NDomainModule := NBinaryDomain.
 Module Export NatModule := BinaryNat.
 
 Definition dep_recursion := Nrec.
@@ -112,10 +112,9 @@ Proof.
 intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step.
 Qed.
 
-End BinaryDepRec.
-
-Module BinaryPlus <: PlusSignature.
+End NBinaryDepRec.
 
+Module NBinaryPlus <: NPlusSignature.
 Module Export NatModule := BinaryNat.
 
 Definition plus := Nplus.
@@ -135,10 +134,10 @@ Proof.
 exact Nplus_succ.
 Qed.
 
-End BinaryPlus.
+End NBinaryPlus.
 
-Module BinaryTimes <: TimesSignature.
-Module Export PlusModule := BinaryPlus.
+Module NBinaryTimes <: NTimesSignature.
+Module Export NPlusModule := NBinaryPlus.
 
 Definition times := Nmult.
 
@@ -157,9 +156,9 @@ Proof.
 exact Nmult_Sn_m.
 Qed.
 
-End BinaryTimes.
+End NBinaryTimes.
 
-Module BinaryLt <: LtSignature.
+Module NBinaryLt <: NLtSignature.
 Module Export NatModule := BinaryNat.
 
 Definition lt (m n : N) := less_than (Ncompare m n).
@@ -184,9 +183,9 @@ assert (H2 : lt x y <-> Ncompare x y = Lt);
 pose proof (Ncompare_n_Sm x y) as H. tauto.
 Qed.
 
-End BinaryLt.
+End NBinaryLt.
 
-Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt.
+Module Export NBinaryTimesLtProperties := NTimesLtProperties NBinaryTimes NBinaryLt.
 
 (*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 00248a53c..9927bde0b 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,11 +1,14 @@
 Require Export NDepRec.
-Require Export NTimesLt.
+Require Export NTimesOrder.
+Require Export NMinus.
 Require Export NMiscFunct.
 
-Module PeanoDomain : DomainEqSignature
-  with Definition N := nat
+Module NPeanoDomain <: NDomainEqSignature.
+(*  with Definition N := nat
   with Definition E := (@eq nat)
-  with Definition e := eq_nat_bool.
+  with Definition e := eq_nat_bool.*)
+
+Delimit Scope NatScope with Nat.
 
 Definition N := nat.
 Definition E := (@eq nat).
@@ -26,10 +29,10 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-End PeanoDomain.
+End NPeanoDomain.
 
 Module PeanoNat <: NatSignature.
-Module Export DomainModule := PeanoDomain.
+Module Export NDomainModule := NPeanoDomain.
 
 Definition O := 0.
 Definition S := S.
@@ -80,9 +83,9 @@ Qed.
 
 End PeanoNat.
 
-Module PeanoDepRec <: DepRecSignature.
+Module NPeanoDepRec <: NDepRecSignature.
 
-Module Export DomainModule := PeanoDomain.
+Module Export NDomainModule := NPeanoDomain.
 Module Export NatModule <: NatSignature := PeanoNat.
 
 Definition dep_recursion := nat_rec.
@@ -101,10 +104,9 @@ Proof.
 reflexivity.
 Qed.
 
-End PeanoDepRec.
-
-Module PeanoPlus <: PlusSignature.
+End NPeanoDepRec.
 
+Module NPeanoPlus <: NPlusSignature.
 Module Export NatModule := PeanoNat.
 
 Definition plus := plus.
@@ -124,10 +126,10 @@ Proof.
 reflexivity.
 Qed.
 
-End PeanoPlus.
+End NPeanoPlus.
 
-Module PeanoTimes <: TimesSignature.
-Module Export PlusModule := PeanoPlus.
+Module NPeanoTimes <: NTimesSignature.
+Module Export NPlusModule := NPeanoPlus.
 
 Definition times := mult.
 
@@ -146,9 +148,9 @@ Proof.
 auto.
 Qed.
 
-End PeanoTimes.
+End NPeanoTimes.
 
-Module PeanoLt <: LtSignature.
+Module NPeanoLt <: NLtSignature.
 Module Export NatModule := PeanoNat.
 
 Definition lt := lt_bool.
@@ -168,14 +170,15 @@ Proof.
 exact lt_bool_S.
 Qed.
 
-End PeanoLt.
+End NPeanoLt.
 
-(* Obtaining properties for +, *, <, and their combinations *)
+Module NPeanoPred <: NPredSignature.
 
-Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt.
-Module Export PeanoDepRecTimesProperties :=
-  DepRecTimesProperties PeanoDepRec PeanoTimes.
+(* Obtaining properties for +, *, <, and their combinations *)
 
-(*Module MiscFunctModule := MiscFunctFunctor PeanoNat.*)
-(* The instruction above adds about 1M to the size of the .vo file !!! *)
+Module Export NPeanoTimesLtProperties := NTimesLtProperties NPeanoTimes NPeanoLt.
+Module Export NPeanoDepRecTimesProperties :=
+  NDepRecTimesProperties NPeanoDepRec NPeanoTimes.
 
+Module MiscFunctModule := MiscFunctFunctor PeanoNat.
+(* The instruction above adds about 0.5M to the size of the .vo file !!! *)