Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

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

12 files changed, 348 insertions, 962 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 58dddfcf94..c3e1e223e1 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -12,70 +12,28 @@
 
 Require Export NBase.
 
-Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
+Module NAddPropFunct (Import N : NAxiomsSig).
+Include NBasePropFunct N.
 
-Open Local Scope NatScope.
+Local Open Scope NumScope.
 
-Theorem add_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
-Proof NZadd_wd.
+(** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *)
+(** Now comes theorems valid for natural numbers but not for Z *)
 
-Theorem add_0_l : forall n : N, 0 + n == n.
-Proof NZadd_0_l.
-
-Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m).
-Proof NZadd_succ_l.
-
-(** Theorems that are valid for both natural numbers and integers *)
-
-Theorem add_0_r : forall n : N, n + 0 == n.
-Proof NZadd_0_r.
-
-Theorem add_succ_r : forall n m : N, n + S m == S (n + m).
-Proof NZadd_succ_r.
-
-Theorem add_comm : forall n m : N, n + m == m + n.
-Proof NZadd_comm.
-
-Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
-Proof NZadd_assoc.
-
-Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
-Proof NZadd_shuffle1.
-
-Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
-Proof NZadd_shuffle2.
-
-Theorem add_1_l : forall n : N, 1 + n == S n.
-Proof NZadd_1_l.
-
-Theorem add_1_r : forall n : N, n + 1 == S n.
-Proof NZadd_1_r.
-
-Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
-Proof NZadd_cancel_l.
-
-Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
-Proof NZadd_cancel_r.
-
-(* Theorems that are valid for natural numbers but cannot be proved for Z *)
-
-Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
+Theorem eq_add_0 : forall n m, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
-(* The next command does not work with the axiom add_0_l from NAddSig *)
-rewrite add_0_l. intuition reflexivity.
-intros n IH. rewrite add_succ_l.
-setoid_replace (S (n + m) == 0) with False using relation iff by
+nzsimpl; intuition.
+intros n IH. nzsimpl.
+setoid_replace (S (n + m) == 0) with False by
  (apply -> neg_false; apply neq_succ_0).
-setoid_replace (S n == 0) with False using relation iff by
+setoid_replace (S n == 0) with False by
  (apply -> neg_false; apply neq_succ_0). tauto.
 Qed.
 
 Theorem eq_add_succ :
-  forall n m : N, (exists p : N, n + m == S p) <->
-                    (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
+  forall n m, (exists p, n + m == S p) <->
+              (exists n', n == S n') \/ (exists m', m == S m').
 Proof.
 intros n m; cases n.
 split; intro H.
@@ -88,11 +46,11 @@ left; now exists n.
 exists (n + m); now rewrite add_succ_l.
 Qed.
 
-Theorem eq_add_1 : forall n m : N,
+Theorem eq_add_1 : forall n m,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
 intros n m H.
-assert (H1 : exists p : N, n + m == S p) by now exists 0.
+assert (H1 : exists p, n + m == S p) by now exists 0.
 apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
 apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
@@ -100,7 +58,7 @@ right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
 apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 Qed.
 
-Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
+Theorem succ_add_discr : forall n m, m ~= S (n + m).
 Proof.
 intro n; induct m.
 apply neq_sym. apply neq_succ_0.
@@ -108,49 +66,18 @@ intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
 unfold not in IH; now apply IH.
 Qed.
 
-Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
+Theorem add_pred_l : forall n m, n ~= 0 -> P n + m == P (n + m).
 Proof.
 intros n m; cases n.
 intro H; now elim H.
 intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ.
 Qed.
 
-Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
+Theorem add_pred_r : forall n m, m ~= 0 -> n + P m == P (n + m).
 Proof.
 intros n m H; rewrite (add_comm n (P m));
 rewrite (add_comm n m); now apply add_pred_l.
 Qed.
 
-(* One could define n <= m as exists p : N, p + n == m. Then we have
-dichotomy:
-
-forall n m : N, n <= m \/ m <= n,
-
-i.e.,
-
-forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n)     (1)
-
-We will need (1) in the proof of induction principle for integers
-constructed as pairs of natural numbers. The formula (1) can be proved
-using properties of order and truncated subtraction. Thus, p would be
-m - n or n - m and (1) would hold by theorem sub_add from Sub.v
-depending on whether n <= m or m <= n. However, in proving induction
-for integers constructed from natural numbers we do not need to
-require implementations of order and sub; it is enough to prove (1)
-here. *)
-
-Theorem add_dichotomy :
-  forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n).
-Proof.
-intros n m; induct n.
-left; exists m; apply add_0_r.
-intros n IH.
-destruct IH as [[p H] | [p H]].
-destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
-rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l.
-left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
-right; exists (S p). rewrite add_succ_l; now rewrite H.
-Qed.
-
 End NAddPropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index 59f1c93475..f48b62e614 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -12,103 +12,38 @@
 
 Require Export NOrder.
 
-Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NAddOrderPropFunct (Import N : NAxiomsSig).
+Include NOrderPropFunct N.
+Local Open Scope NumScope.
 
-Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
-Proof NZadd_lt_mono_l.
+(** Theorems true for natural numbers, not for integers *)
 
-Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.
-Proof NZadd_lt_mono_r.
-
-Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.
-Proof NZadd_lt_mono.
-
-Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.
-Proof NZadd_le_mono_l.
-
-Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.
-Proof NZadd_le_mono_r.
-
-Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.
-Proof NZadd_le_mono.
-
-Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.
-Proof NZadd_lt_le_mono.
-
-Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
-Proof NZadd_le_lt_mono.
-
-Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.
-Proof NZadd_pos_pos.
-
-Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m.
-Proof NZlt_add_pos_l.
-
-Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n.
-Proof NZlt_add_pos_r.
-
-Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
-Proof NZle_lt_add_lt.
-
-Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
-Proof NZlt_le_add_lt.
-
-Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_add_le.
-
-Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
-Proof NZadd_lt_cases.
-
-Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
-Proof NZadd_le_cases.
-
-Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZadd_pos_cases.
-
-(* Theorems true for natural numbers *)
-
-Theorem le_add_r : forall n m : N, n <= n + m.
+Theorem le_add_r : forall n m, n <= n + m.
 Proof.
 intro n; induct m.
 rewrite add_0_r; now apply eq_le_incl.
 intros m IH. rewrite add_succ_r; now apply le_le_succ_r.
 Qed.
 
-Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p.
+Theorem lt_lt_add_r : forall n m p, n < m -> n < m + p.
 Proof.
 intros n m p H; rewrite <- (add_0_r n).
 apply add_lt_le_mono; [assumption | apply le_0_l].
 Qed.
 
-Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m.
+Theorem lt_lt_add_l : forall n m p, n < m -> n < p + m.
 Proof.
 intros n m p; rewrite add_comm; apply lt_lt_add_r.
 Qed.
 
-Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m.
+Theorem add_pos_l : forall n m, 0 < n -> 0 < n + m.
 Proof.
-intros; apply NZadd_pos_nonneg. assumption. apply le_0_l.
+intros; apply add_pos_nonneg. assumption. apply le_0_l.
 Qed.
 
-Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m.
-Proof.
-intros; apply NZadd_nonneg_pos. apply le_0_l. assumption.
-Qed.
-
-(* The following property is used to prove the correctness of the
-definition of order on integers constructed from pairs of natural numbers *)
-
-Theorem add_lt_repl_pair : forall n m n' m' u v : N,
-  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
+Theorem add_pos_r : forall n m, 0 < m -> 0 < n + m.
 Proof.
-intros n m n' m' u v H1 H2.
-symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl.
-pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4.
-rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4.
-do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4.
-now rewrite (add_comm n' u), (add_comm m' v).
+intros; apply add_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
 End NAddOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 6a34d0f7b6..bdabb1086d 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -15,54 +15,24 @@ Require Export NZAxioms.
 Set Implicit Arguments.
 
 Module Type NAxiomsSig.
-Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
+Include Type NZOrdAxiomsSig.
+Local Open Scope NumScope.
 
-Delimit Scope NatScope with Nat.
-Notation N := NZ.
-Notation Neq := NZeq.
-Notation N0 := NZ0.
-Notation N1 := (NZsucc NZ0).
-Notation S := NZsucc.
-Notation P := NZpred.
-Notation add := NZadd.
-Notation mul := NZmul.
-Notation sub := NZsub.
-Notation lt := NZlt.
-Notation le := NZle.
-Notation min := NZmin.
-Notation max := NZmax.
-Notation "x == y"  := (Neq x y) (at level 70) : NatScope.
-Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope.
-Notation "0" := NZ0 : NatScope.
-Notation "1" := (NZsucc NZ0) : NatScope.
-Notation "x + y" := (NZadd x y) : NatScope.
-Notation "x - y" := (NZsub x y) : NatScope.
-Notation "x * y" := (NZmul x y) : NatScope.
-Notation "x < y" := (NZlt x y) : NatScope.
-Notation "x <= y" := (NZle x y) : NatScope.
-Notation "x > y" := (NZlt y x) (only parsing) : NatScope.
-Notation "x >= y" := (NZle y x) (only parsing) : NatScope.
-
-Open Local Scope NatScope.
+Axiom pred_0 : P 0 == 0.
 
-Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> A.
+Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
 Implicit Arguments recursion [A].
 
-Axiom pred_0 : P 0 == 0.
-
 Instance recursion_wd (A : Type) (Aeq : relation A) :
- Proper (Aeq ==> (Neq==>Aeq==>Aeq) ==> Neq ==> Aeq) (@recursion A).
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 
 Axiom recursion_0 :
-  forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+  forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a.
 
 Axiom recursion_succ :
-  forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
-    Aeq a a -> Proper (Neq==>Aeq==>Aeq) f ->
-      forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
-
-(*Axiom dep_rec :
-  forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*)
+  forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A),
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
+      forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
 End NAxiomsSig.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 02d82bacde..6bf12ee5ea 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -12,131 +12,75 @@
 
 Require Export Decidable.
 Require Export NAxioms.
-Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *)
+Require Import NZProperties.
 
-Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
+Module NBasePropFunct (Import N : NAxiomsSig).
+(** First, we import all known facts about both natural numbers and integers. *)
+Include NZPropFunct N.
+Local Open Scope NumScope.
 
-Open Local Scope NatScope.
-
-(* We call the last property functor on NZ, which includes all the previous
-ones, to get all properties of NZ at once. This way we will include them
-only one time. *)
-
-Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod.
-
-(* Here we probably need to re-prove all axioms declared in NAxioms.v to
-make sure that the definitions like N, S and add are unfolded in them,
-since unfolding is done only inside a functor. In fact, we'll do it in the
-files that prove the corresponding properties. In those files, we will also
-rename properties proved in NZ files by removing NZ from their names. In
-this way, one only has to consult, for example, NAdd.v to see all
-available properties for add, i.e., one does not have to go to NAxioms.v
-for axioms and NZAdd.v for theorems. *)
-
-Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2.
-Proof NZsucc_wd.
-
-Theorem pred_wd : forall n1 n2 : N, n1 == n2 -> P n1 == P n2.
-Proof NZpred_wd.
-
-Theorem pred_succ : forall n : N, P (S n) == n.
-Proof NZpred_succ.
-
-Theorem pred_0 : P 0 == 0.
-Proof pred_0.
-
-Theorem Neq_refl : forall n : N, n == n.
-Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
-
-Theorem Neq_sym : forall n m : N, n == m -> m == n.
-Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
-
-Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
-Proof (@Equivalence_Transitive _ _ NZeq_equiv).
-
-Theorem neq_sym : forall n m : N, n ~= m -> m ~= n.
-Proof NZneq_sym.
-
-Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2.
-Proof NZsucc_inj.
-
-Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2.
-Proof NZsucc_inj_wd.
-
-Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
-Proof NZsucc_inj_wd_neg.
-
-(* Decidability and stability of equality was proved only in NZOrder, but
-since it does not mention order, we'll put it here *)
-
-Theorem eq_dec : forall n m : N, decidable (n == m).
-Proof NZeq_dec.
-
-Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m.
-Proof NZeq_dne.
-
-(* Now we prove that the successor of a number is not zero by defining a
+(** We prove that the successor of a number is not zero by defining a
 function (by recursion) that maps 0 to false and the successor to true *)
 
-Definition if_zero (A : Set) (a b : A) (n : N) : A :=
+Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
   recursion a (fun _ _ => b) n.
 
-Instance if_zero_wd (A : Set) : Proper (eq ==> eq ==> Neq ==> eq) (if_zero A).
+Implicit Arguments if_zero [A].
+
+Instance if_zero_wd (A : Type) :
+ Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
 Proof.
 intros; unfold if_zero.
 repeat red; intros. apply recursion_wd; auto. repeat red; auto.
 Qed.
 
-Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
+Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.
 Proof.
 unfold if_zero; intros; now rewrite recursion_0.
 Qed.
 
-Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
+Theorem if_zero_succ :
+ forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b.
 Proof.
 intros; unfold if_zero.
-now rewrite (@recursion_succ A (@eq A)).
+now rewrite recursion_succ.
 Qed.
 
-Implicit Arguments if_zero [A].
-
-Theorem neq_succ_0 : forall n : N, S n ~= 0.
+Theorem neq_succ_0 : forall n, S n ~= 0.
 Proof.
 intros n H.
-assert (true = false); [| discriminate].
-replace true with (if_zero false true (S n)) by apply if_zero_succ.
-pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0.
-now rewrite H.
+generalize (Logic.eq_refl (if_zero false true 0)).
+rewrite <- H at 1. rewrite if_zero_0, if_zero_succ; discriminate.
 Qed.
 
-Theorem neq_0_succ : forall n : N, 0 ~= S n.
+Theorem neq_0_succ : forall n, 0 ~= S n.
 Proof.
 intro n; apply neq_sym; apply neq_succ_0.
 Qed.
 
-(* Next, we show that all numbers are nonnegative and recover regular induction
-from the bidirectional induction on NZ *)
+(** Next, we show that all numbers are nonnegative and recover regular
+    induction from the bidirectional induction on NZ *)
 
-Theorem le_0_l : forall n : N, 0 <= n.
+Theorem le_0_l : forall n, 0 <= n.
 Proof.
-NZinduct n.
-now apply NZeq_le_incl.
+nzinduct n.
+now apply eq_le_incl.
 intro n; split.
-apply NZle_le_succ_r.
-intro H; apply -> NZle_succ_r in H; destruct H as [H | H].
+apply le_le_succ_r.
+intro H; apply -> le_succ_r in H; destruct H as [H | H].
 assumption.
 symmetry in H; false_hyp H neq_succ_0.
 Qed.
 
 Theorem induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
+  forall A : N.t -> Prop, Proper (N.eq==>iff) A ->
+    A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
 Proof.
-intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption.
+intros A A_wd A0 AS n; apply right_induction with 0; try assumption.
 intros; auto; apply le_0_l. apply le_0_l.
 Qed.
 
-(* The theorems NZinduction, NZcentral_induction and the tactic NZinduct
+(** The theorems [bi_induction], [central_induction] and the tactic [nzinduct]
 refer to bidirectional induction, which is not useful on natural
 numbers. Therefore, we define a new induction tactic for natural numbers.
 We do not have to call "Declare Left Step" and "Declare Right Step"
@@ -146,8 +90,8 @@ from NZ. *)
 Ltac induct n := induction_maker n ltac:(apply induction).
 
 Theorem case_analysis :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
+  forall A : N.t -> Prop, Proper (N.eq==>iff) A ->
+    A 0 -> (forall n, A (S n)) -> forall n, A n.
 Proof.
 intros; apply induction; auto.
 Qed.
@@ -173,7 +117,7 @@ now left.
 intro n; right; now exists n.
 Qed.
 
-Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1.
+Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.
 Proof.
 cases n.
 rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
@@ -184,14 +128,14 @@ setoid_replace (S n == 0) with False using relation iff by
 rewrite succ_inj_wd. tauto.
 Qed.
 
-Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n.
+Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.
 Proof.
 cases n.
 intro H; exfalso; now apply H.
 intros; now rewrite pred_succ.
 Qed.
 
-Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
+Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
 Proof.
 intros n m; cases n.
 intros H; exfalso; now apply H.
@@ -200,13 +144,13 @@ intros H; exfalso; now apply H.
 intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3.
 Qed.
 
-(* The following induction principle is useful for reasoning about, e.g.,
+(** The following induction principle is useful for reasoning about, e.g.,
 Fibonacci numbers *)
 
 Section PairInduction.
 
-Variable A : N -> Prop.
-Hypothesis A_wd : Proper (Neq==>iff) A.
+Variable A : N.t -> Prop.
+Hypothesis A_wd : Proper (N.eq==>iff) A.
 
 Theorem pair_induction :
   A 0 -> A 1 ->
@@ -219,13 +163,12 @@ Qed.
 
 End PairInduction.
 
-(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*)
+(** The following is useful for reasoning about, e.g., Ackermann function *)
 
-(* The following is useful for reasoning about, e.g., Ackermann function *)
 Section TwoDimensionalInduction.
 
-Variable R : N -> N -> Prop.
-Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
+Variable R : N.t -> N.t -> Prop.
+Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.
 
 Theorem two_dim_induction :
    R 0 0 ->
@@ -241,21 +184,16 @@ Qed.
 
 End TwoDimensionalInduction.
 
-(*Ltac two_dim_induct n m :=
-  try intros until n;
-  try intros until m;
-  pattern n, m; apply two_dim_induction; clear n m;
-  [solve_relation_wd | | | ].*)
 
 Section DoubleInduction.
 
-Variable R : N -> N -> Prop.
-Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
+Variable R : N.t -> N.t -> Prop.
+Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.
 
 Theorem double_induction :
-   (forall m : N, R 0 m) ->
-   (forall n : N, R (S n) 0) ->
-   (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m.
+   (forall m, R 0 m) ->
+   (forall n, R (S n) 0) ->
+   (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m.
 Proof.
 intros H1 H2 H3; induct n; auto.
 intros n H; cases m; auto.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e864b66d5f..1239173752 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -13,48 +13,42 @@
 Require Import Bool. (* To get the orb and negb function *)
 Require Export NStrongRec.
 
-Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod.
-Local Open Scope NatScope.
-
-Hint Rewrite
- add_0_l add_0_r add_succ_l add_succ_r
- mul_0_l mul_0_r mul_succ_l mul_succ_l : numbers.
-
-Ltac nsimpl := autorewrite with numbers.
+Module NdefOpsPropFunct (Import N : NAxiomsSig).
+Include NStrongRecPropFunct N.
+Local Open Scope NumScope.
 
 (*****************************************************)
 (**                   Addition                       *)
 
-Definition def_add (x y : N) := recursion y (fun _ => S) x.
+Definition def_add (x y : N.t) := recursion y (fun _ => S) x.
 
 Local Infix "+++" := def_add (at level 50, left associativity).
 
-Instance def_add_prewd : Proper (Neq==>Neq==>Neq) (fun _ => S).
+Instance def_add_prewd : Proper (N.eq==>N.eq==>N.eq) (fun _ => S).
 Proof.
 intros _ _ _ p p' Epp'; now rewrite Epp'.
 Qed.
 
-Instance def_add_wd : Proper (Neq ==> Neq ==> Neq) def_add.
+Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add.
 Proof.
 intros x x' Exx' y y' Eyy'. unfold def_add.
 (* TODO: why rewrite Exx' don't work here (or verrrry slowly) ? *)
-apply recursion_wd with (Aeq := Neq); auto with *.
+apply recursion_wd with (Aeq := N.eq); auto with *.
 apply def_add_prewd.
 Qed.
 
-Theorem def_add_0_l : forall y : N, 0 +++ y == y.
+Theorem def_add_0_l : forall y, 0 +++ y == y.
 Proof.
 intro y. unfold def_add. now rewrite recursion_0.
 Qed.
 
-Theorem def_add_succ_l : forall x y : N, S x +++ y == S (x +++ y).
+Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y).
 Proof.
 intros x y; unfold def_add.
 rewrite recursion_succ; auto with *.
 Qed.
 
-Theorem def_add_add : forall n m : N, n +++ m == n + m.
+Theorem def_add_add : forall n m, n +++ m == n + m.
 Proof.
 intros n m; induct n.
 now rewrite def_add_0_l, add_0_l.
@@ -64,17 +58,17 @@ Qed.
 (*****************************************************)
 (**                  Multiplication                  *)
 
-Definition def_mul (x y : N) := recursion 0 (fun _ p => p +++ x) y.
+Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y.
 
 Local Infix "**" := def_mul (at level 40, left associativity).
 
 Instance def_mul_prewd :
- Proper (Neq==>Neq==>Neq==>Neq) (fun x _ p => p +++ x).
+ Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun x _ p => p +++ x).
 Proof.
 repeat red; intros; now apply def_add_wd.
 Qed.
 
-Instance def_mul_wd : Proper (Neq ==> Neq ==> Neq) def_mul.
+Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul.
 Proof.
 unfold def_mul.
 intros x x' Exx' y y' Eyy'.
@@ -82,19 +76,19 @@ apply recursion_wd; auto with *.
 now apply def_mul_prewd.
 Qed.
 
-Theorem def_mul_0_r : forall x : N, x ** 0 == 0.
+Theorem def_mul_0_r : forall x, x ** 0 == 0.
 Proof.
 intro. unfold def_mul. now rewrite recursion_0.
 Qed.
 
-Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y +++ x.
+Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x.
 Proof.
 intros x y; unfold def_mul.
 rewrite recursion_succ; auto with *.
 now apply def_mul_prewd.
 Qed.
 
-Theorem def_mul_mul : forall n m : N, n ** m == n * m.
+Theorem def_mul_mul : forall n m, n ** m == n * m.
 Proof.
 intros n m; induct m.
 now rewrite def_mul_0_r, mul_0_r.
@@ -104,7 +98,7 @@ Qed.
 (*****************************************************)
 (**                     Order                        *)
 
-Definition ltb (m : N) : N -> bool :=
+Definition ltb (m : N.t) : N.t -> bool :=
 recursion
   (if_zero false true)
   (fun _ f n => recursion false (fun n' _ => f n') n)
@@ -112,12 +106,12 @@ recursion
 
 Local Infix "<<" := ltb (at level 70, no associativity).
 
-Instance ltb_prewd1 : Proper (Neq==>eq) (if_zero false true).
+Instance ltb_prewd1 : Proper (N.eq==>Logic.eq) (if_zero false true).
 Proof.
 red; intros; apply if_zero_wd; auto.
 Qed.
 
-Instance ltb_prewd2 : Proper (Neq==>(Neq==>eq)==>Neq==>eq)
+Instance ltb_prewd2 : Proper (N.eq==>(N.eq==>Logic.eq)==>N.eq==>Logic.eq)
  (fun _ f n => recursion false (fun n' _ => f n') n).
 Proof.
 repeat red; intros; simpl.
@@ -125,7 +119,7 @@ apply recursion_wd; auto with *.
 repeat red; auto.
 Qed.
 
-Instance ltb_wd : Proper (Neq ==> Neq ==> eq) ltb.
+Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb.
 Proof.
 unfold ltb.
 intros n n' Hn m m' Hm.
@@ -133,13 +127,13 @@ apply f_equiv; auto with *.
 apply recursion_wd; auto; [ apply ltb_prewd1 | apply ltb_prewd2 ].
 Qed.
 
-Theorem ltb_base : forall n : N, 0 << n = if_zero false true n.
+Theorem ltb_base : forall n, 0 << n = if_zero false true n.
 Proof.
 intro n; unfold ltb; now rewrite recursion_0.
 Qed.
 
 Theorem ltb_step :
-  forall m n : N, S m << n = recursion false (fun n' _ => m << n') n.
+  forall m n, S m << n = recursion false (fun n' _ => m << n') n.
 Proof.
 intros m n; unfold ltb at 1.
 apply f_equiv; auto with *.
@@ -153,26 +147,26 @@ Qed.
 functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
 lt_step n (recursion lt_base lt_step n)? *)
 
-Theorem ltb_0 : forall n : N, n << 0 = false.
+Theorem ltb_0 : forall n, n << 0 = false.
 Proof.
 cases n.
 rewrite ltb_base; now rewrite if_zero_0.
 intro n; rewrite ltb_step. now rewrite recursion_0.
 Qed.
 
-Theorem ltb_0_succ : forall n : N, 0 << S n = true.
+Theorem ltb_0_succ : forall n, 0 << S n = true.
 Proof.
 intro n; rewrite ltb_base; now rewrite if_zero_succ.
 Qed.
 
-Theorem succ_ltb_mono : forall n m : N, (S n << S m) = (n << m).
+Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m).
 Proof.
 intros n m.
 rewrite ltb_step. rewrite recursion_succ; try reflexivity.
 repeat red; intros; now apply ltb_wd.
 Qed.
 
-Theorem ltb_lt : forall n m : N, n << m = true <-> n < m.
+Theorem ltb_lt : forall n m, n << m = true <-> n < m.
 Proof.
 double_induct n m.
 cases m.
@@ -186,9 +180,9 @@ Qed.
 (*****************************************************)
 (**                     Even                         *)
 
-Definition even (x : N) := recursion true (fun _ p => negb p) x.
+Definition even (x : N.t) := recursion true (fun _ p => negb p) x.
 
-Instance even_wd : Proper (Neq==>eq) even.
+Instance even_wd : Proper (N.eq==>Logic.eq) even.
 Proof.
 intros n n' Hn. unfold even.
 apply recursion_wd; auto.
@@ -201,7 +195,7 @@ unfold even.
 now rewrite recursion_0.
 Qed.
 
-Theorem even_succ : forall x : N, even (S x) = negb (even x).
+Theorem even_succ : forall x, even (S x) = negb (even x).
 Proof.
 unfold even.
 intro x; rewrite recursion_succ; try reflexivity.
@@ -217,12 +211,12 @@ Local Notation "a < b <= c" := (a<b /\ b<=c).
 Local Notation "a < b < c" := (a<b /\ b<c).
 Local Notation "2" := (S 1).
 
-Definition half_aux (x : N) : N * N :=
+Definition half_aux (x : N.t) : N.t * N.t :=
   recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x.
 
-Definition half (x : N) := snd (half_aux x).
+Definition half (x : N.t) := snd (half_aux x).
 
-Instance half_aux_wd : Proper (Neq ==> Neq*Neq) half_aux.
+Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux.
 Proof.
 intros x x' Hx. unfold half_aux.
 apply recursion_wd; auto with *.
@@ -230,7 +224,7 @@ intros y y' Hy (u,v) (u',v') (Hu,Hv). compute in *.
 rewrite Hu, Hv; auto with *.
 Qed.
 
-Instance half_wd : Proper (Neq==>Neq) half.
+Instance half_wd : Proper (N.eq==>N.eq) half.
 Proof.
 intros x x' Hx. unfold half. rewrite Hx; auto with *.
 Qed.
@@ -290,7 +284,7 @@ Theorem half_double : forall n,
  n == 2 * half n \/ n == 1 + 2 * half n.
 Proof.
 intros. unfold half.
-nsimpl.
+nzsimpl.
 destruct (half_aux_spec2 n) as [H|H]; [left|right].
 rewrite <- H at 1. apply half_aux_spec.
 rewrite <- add_succ_l. rewrite <- H at 1. apply half_aux_spec.
@@ -301,7 +295,7 @@ Proof.
 intros.
 destruct (half_double n) as [E|E]; rewrite E at 2.
 apply le_refl.
-nsimpl.
+nzsimpl.
 apply le_le_succ_r, le_refl.
 Qed.
 
@@ -309,7 +303,7 @@ Theorem half_lower_bound : forall n, n <= 1 + 2 * half n.
 Proof.
 intros.
 destruct (half_double n) as [E|E]; rewrite E at 1.
-nsimpl.
+nzsimpl.
 apply le_le_succ_r, le_refl.
 apply le_refl.
 Qed.
@@ -345,17 +339,17 @@ Qed.
 (*****************************************************)
 (**            Power                                 *)
 
-Definition pow (n m : N) := recursion 1 (fun _ r => n*r) m.
+Definition pow (n m : N.t) := recursion 1 (fun _ r => n*r) m.
 
 Local Infix "^^" := pow (at level 30, right associativity).
 
 Instance pow_prewd :
- Proper (Neq==>Neq==>Neq==>Neq) (fun n _ r => n*r).
+ Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun n _ r => n*r).
 Proof.
 intros n n' Hn x x' Hx y y' Hy. rewrite Hn, Hy; auto with *.
 Qed.
 
-Instance pow_wd : Proper (Neq==>Neq==>Neq) pow.
+Instance pow_wd : Proper (N.eq==>N.eq==>N.eq) pow.
 Proof.
 intros n n' Hn m m' Hm. unfold pow.
 apply recursion_wd; auto with *.
@@ -377,7 +371,7 @@ Qed.
 (*****************************************************)
 (**            Logarithm for the base 2              *)
 
-Definition log (x : N) : N :=
+Definition log (x : N.t) : N.t :=
 strong_rec 0
            (fun g x =>
               if x << 2 then 0
@@ -385,7 +379,7 @@ strong_rec 0
            x.
 
 Instance log_prewd :
- Proper ((Neq==>Neq)==>Neq==>Neq)
+ Proper ((N.eq==>N.eq)==>N.eq==>N.eq)
    (fun g x => if x<<2 then 0 else S (g (half x))).
 Proof.
 intros g g' Hg n n' Hn.
@@ -395,7 +389,7 @@ apply succ_wd.
 apply Hg. rewrite Hn; auto with *.
 Qed.
 
-Instance log_wd : Proper (Neq==>Neq) log.
+Instance log_wd : Proper (N.eq==>N.eq) log.
 Proof.
 intros x x' Exx'. unfold log.
 apply strong_rec_wd; auto with *.
@@ -403,7 +397,7 @@ apply log_prewd.
 Qed.
 
 Lemma log_good_step : forall n h1 h2,
- (forall m : N, m < n -> h1 m == h2 m) ->
+ (forall m, m < n -> h1 m == h2 m) ->
   (if n << 2 then 0 else S (h1 (half n))) ==
   (if n << 2 then 0 else S (h2 (half n))).
 Proof.
@@ -460,10 +454,10 @@ split.
 rewrite <- le_succ_l in IH1.
 apply mul_le_mono_l with (p:=2) in IH1.
 eapply lt_le_trans; eauto.
-nsimpl.
+nzsimpl.
 rewrite lt_succ_r.
 eapply le_trans; [ eapply half_lower_bound | ].
-nsimpl; apply le_refl.
+nzsimpl; apply le_refl.
 eapply le_trans; [ | eapply half_upper_bound ].
 apply mul_le_mono_l; auto.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 6ecf7fd338..13e289c295 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -12,47 +12,37 @@
 
 Require Import NBase.
 
-Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
+Module Homomorphism (N1 N2 : NAxiomsSig).
 
-Module NBasePropMod2 := NBasePropFunct NAxiomsMod2.
+Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).
 
-Notation Local N1 := NAxiomsMod1.N.
-Notation Local N2 := NAxiomsMod2.N.
-Notation Local Eq1 := NAxiomsMod1.Neq.
-Notation Local Eq2 := NAxiomsMod2.Neq.
-Notation Local O1 := NAxiomsMod1.N0.
-Notation Local O2 := NAxiomsMod2.N0.
-Notation Local S1 := NAxiomsMod1.S.
-Notation Local S2 := NAxiomsMod2.S.
-Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity).
+Definition homomorphism (f : N1.t -> N2.t) : Prop :=
+  f N1.zero == N2.zero /\ forall n, f (N1.S n) == N2.S (f n).
 
-Definition homomorphism (f : N1 -> N2) : Prop :=
-  f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n).
+Definition natural_isomorphism : N1.t -> N2.t :=
+  N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.S p).
 
-Definition natural_isomorphism : N1 -> N2 :=
-  NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).
-
-Instance natural_isomorphism_wd : Proper (Eq1 ==> Eq2) natural_isomorphism.
+Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.
 Proof.
 unfold natural_isomorphism.
 intros n m Eqxy.
-apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
+apply N1.recursion_wd.
 reflexivity.
-intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
+intros _ _ _ y' y'' H. now apply N2.succ_wd.
 assumption.
 Qed.
 
-Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2.
+Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero.
 Proof.
-unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0.
+unfold natural_isomorphism; now rewrite N1.recursion_0.
 Qed.
 
 Theorem natural_isomorphism_succ :
-  forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
+  forall n : N1.t, natural_isomorphism (N1.S n) == N2.S (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); auto with *.
-repeat red; intros. apply NBasePropMod2.succ_wd; auto.
+intro n. rewrite N1.recursion_succ; auto with *.
+repeat red; intros. apply N2.succ_wd; auto.
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
@@ -63,23 +53,20 @@ Qed.
 
 End Homomorphism.
 
-Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
+Module Inverse (N1 N2 : NAxiomsSig).
 
-Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1.
+Module Import NBasePropMod1 := NBasePropFunct N1.
 (* This makes the tactic induct available. Since it is taken from
 (NBasePropFunct NAxiomsMod1), it refers to induction on N1. *)
 
-Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
-Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
-
-Notation Local N1 := NAxiomsMod1.N.
-Notation Local N2 := NAxiomsMod2.N.
-Notation Local h12 := Hom12.natural_isomorphism.
-Notation Local h21 := Hom21.natural_isomorphism.
+Module Hom12 := Homomorphism N1 N2.
+Module Hom21 := Homomorphism N2 N1.
 
-Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity).
+Local Notation h12 := Hom12.natural_isomorphism.
+Local Notation h21 := Hom21.natural_isomorphism.
+Local Notation "n == m" := (N1.eq n m) (at level 70, no associativity).
 
-Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n.
+Lemma inverse_nat_iso : forall n : N1.t, h21 (h12 n) == n.
 Proof.
 induct n.
 now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0.
@@ -89,25 +76,20 @@ Qed.
 
 End Inverse.
 
-Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
-
-Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
-Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
+Module Isomorphism (N1 N2 : NAxiomsSig).
 
-Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2.
-Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1.
+Module Hom12 := Homomorphism N1 N2.
+Module Hom21 := Homomorphism N2 N1.
+Module Inverse12 := Inverse N1 N2.
+Module Inverse21 := Inverse N2 N1.
 
-Notation Local N1 := NAxiomsMod1.N.
-Notation Local N2 := NAxiomsMod2.N.
-Notation Local Eq1 := NAxiomsMod1.Neq.
-Notation Local Eq2 := NAxiomsMod2.Neq.
-Notation Local h12 := Hom12.natural_isomorphism.
-Notation Local h21 := Hom21.natural_isomorphism.
+Local Notation h12 := Hom12.natural_isomorphism.
+Local Notation h21 := Hom21.natural_isomorphism.
 
-Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop :=
+Definition isomorphism (f1 : N1.t -> N2.t) (f2 : N2.t -> N1.t) : Prop :=
   Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
-  forall n : N1, Eq1 (f2 (f1 n)) n /\
-  forall n : N2, Eq2 (f1 (f2 n)) n.
+  forall n, N1.eq (f2 (f1 n)) n /\
+  forall n, N2.eq (f1 (f2 n)) n.
 
 Theorem iso_nat_iso : isomorphism h12 h21.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v
deleted file mode 100644
index 69b284fdcf..0000000000
--- a/theories/Numbers/Natural/Abstract/NMul.v
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export NAdd.
-
-Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NAddPropMod := NAddPropFunct NAxiomsMod.
-Open Local Scope NatScope.
-
-Theorem mul_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2.
-Proof NZmul_wd.
-
-Theorem mul_0_l : forall n : N, 0 * n == 0.
-Proof NZmul_0_l.
-
-Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m.
-Proof NZmul_succ_l.
-
-(** Theorems that are valid for both natural numbers and integers *)
-
-Theorem mul_0_r : forall n, n * 0 == 0.
-Proof NZmul_0_r.
-
-Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
-Proof NZmul_succ_r.
-
-Theorem mul_comm : forall n m : N, n * m == m * n.
-Proof NZmul_comm.
-
-Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p.
-Proof NZmul_add_distr_r.
-
-Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p.
-Proof NZmul_add_distr_l.
-
-Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p.
-Proof NZmul_assoc.
-
-Theorem mul_1_l : forall n : N, 1 * n == n.
-Proof NZmul_1_l.
-
-Theorem mul_1_r : forall n : N, n * 1 == n.
-Proof NZmul_1_r.
-
-(* Theorems that cannot be proved in NZMul *)
-
-(* 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 * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v
-
-Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'),
-since a pair (a, b) of natural numbers represents the integer a - b. On
-integers, the formula above could be proved by moving a * m to the left,
-factoring out a and replacing n - m by n' - m'. However, the formula is
-required in the process of constructing integers, so it has to be proved
-for natural numbers, where terms cannot be moved from one side of an
-equation to the other. The proof uses the cancellation laws add_cancel_l
-and add_cancel_r. *)
-
-Theorem add_mul_repl_pair : forall a n m n' m' u v : N,
-  a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
-Proof.
-intros a n m n' m' u v H1 H2.
-apply (@NZmul_wd a a) in H2; [| reflexivity].
-do 2 rewrite mul_add_distr_l in H2. symmetry in H2.
-pose proof (NZadd_wd _ _ H1 _ _ H2) as H3.
-rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3.
-do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3.
-rewrite (add_assoc u), (add_comm (a * m)) in H3.
-apply -> add_cancel_r in H3.
-now rewrite (add_comm (a * n') u), (add_comm (a * m') v).
-Qed.
-
-End NMulPropFunct.
-
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index ac4cc5e9ed..285d8c1049 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -12,118 +12,68 @@
 
 Require Export NAddOrder.
 
-Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NMulOrderPropFunct (Import N : NAxiomsSig).
+Include NAddOrderPropFunct N.
+Local Open Scope NumScope.
 
-Theorem mul_lt_pred :
-  forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZmul_lt_pred.
+(** Theorems that are either not valid on Z or have different proofs
+    on N and Z *)
 
-Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZmul_lt_mono_pos_l.
-
-Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZmul_lt_mono_pos_r.
-
-Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZmul_cancel_l.
-
-Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
-Proof NZmul_cancel_r.
-
-Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1).
-Proof NZmul_id_l.
-
-Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1).
-Proof NZmul_id_r.
-
-Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZmul_le_mono_pos_l.
-
-Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZmul_le_mono_pos_r.
-
-Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZmul_pos_pos.
-
-Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m.
-Proof NZlt_1_mul_pos.
-
-Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_mul_0.
-
-Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_mul_0.
-
-Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0.
-Proof NZeq_square_0.
-
-Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
-Proof NZeq_mul_0_l.
-
-Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0.
-Proof NZeq_mul_0_r.
-
-Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m.
+Theorem square_lt_mono : forall n m, n < m <-> n * n < m * m.
 Proof.
 intros n m; split; intro;
-[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg];
+[apply square_lt_mono_nonneg | apply square_lt_simpl_nonneg];
 try assumption; apply le_0_l.
 Qed.
 
-Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m.
+Theorem square_le_mono : forall n m, n <= m <-> n * n <= m * m.
 Proof.
 intros n m; split; intro;
-[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg];
+[apply square_le_mono_nonneg | apply square_le_simpl_nonneg];
 try assumption; apply le_0_l.
 Qed.
 
-Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
-Proof NZmul_2_mono_l.
-
-(* Theorems that are either not valid on Z or have different proofs on N and Z *)
-
-Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
+Theorem mul_le_mono_l : forall n m p, n <= m -> p * n <= p * m.
 Proof.
-intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption.
+intros; apply mul_le_mono_nonneg_l. apply le_0_l. assumption.
 Qed.
 
-Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p.
+Theorem mul_le_mono_r : forall n m p, n <= m -> n * p <= m * p.
 Proof.
-intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption.
+intros; apply mul_le_mono_nonneg_r. apply le_0_l. assumption.
 Qed.
 
-Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
+Theorem mul_lt_mono : forall n m p q, n < m -> p < q -> n * p < m * q.
 Proof.
-intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l.
+intros; apply mul_lt_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
-Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q.
+Theorem mul_le_mono : forall n m p q, n <= m -> p <= q -> n * p <= m * q.
 Proof.
-intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l.
+intros; apply mul_le_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
-Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
+Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
-apply -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
-now apply NZmul_pos_pos.
+apply -> lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split.
+ false_hyp H1 nlt_0_r.
+now apply mul_pos_pos.
 Qed.
 
-Notation mul_pos := lt_0_mul (only parsing).
+Notation mul_pos := lt_0_mul' (only parsing).
 
-Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1.
+Theorem eq_mul_1 : forall n m, n * m == 1 <-> n == 1 /\ m == 1.
 Proof.
 intros n m.
 split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l].
-intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]].
+intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]].
 apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ.
 rewrite H1, mul_1_l in H; now split.
 destruct (eq_0_gt_0_cases m) as [H2 | H2].
 rewrite H2, mul_0_r in H; false_hyp H neq_0_succ.
 apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
-assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m).
+assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index a5b496ba32..94c68a1867 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -10,352 +10,61 @@
 
 (*i $Id$ i*)
 
-Require Export NMul.
+Require Export NAdd.
 
-Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NMulPropMod := NMulPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NOrderPropFunct (Import N : NAxiomsSig).
+Include NAddPropFunct N.
+Local Open Scope NumScope.
 
-(* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
-
-(* Axioms *)
-
-Theorem lt_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 < m1 <-> n2 < m2).
-Proof NZlt_wd.
-
-Theorem le_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
-Proof NZle_wd.
-
-Theorem min_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> min n1 m1 == min n2 m2.
-Proof NZmin_wd.
-
-Theorem max_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2.
-Proof NZmax_wd.
-
-Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m.
-Proof NZlt_eq_cases.
-
-Theorem lt_irrefl : forall n : N, ~ n < n.
-Proof NZlt_irrefl.
-
-Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m.
-Proof NZlt_succ_r.
-
-Theorem min_l : forall n m : N, n <= m -> min n m == n.
-Proof NZmin_l.
-
-Theorem min_r : forall n m : N, m <= n -> min n m == m.
-Proof NZmin_r.
-
-Theorem max_l : forall n m : N, m <= n -> max n m == n.
-Proof NZmax_l.
-
-Theorem max_r : forall n m : N, n <= m -> max n m == m.
-Proof NZmax_r.
-
-(* Renaming theorems from NZOrder.v *)
-
-Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
-Proof NZlt_le_incl.
-
-Theorem eq_le_incl : forall n m : N, n == m -> n <= m.
-Proof NZeq_le_incl.
-
-Theorem lt_neq : forall n m : N, n < m -> n ~= m.
-Proof NZlt_neq.
-
-Theorem le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
-Proof NZle_neq.
-
-Theorem le_refl : forall n : N, n <= n.
-Proof NZle_refl.
-
-Theorem lt_succ_diag_r : forall n : N, n < S n.
-Proof NZlt_succ_diag_r.
-
-Theorem le_succ_diag_r : forall n : N, n <= S n.
-Proof NZle_succ_diag_r.
-
-Theorem lt_0_1 : 0 < 1.
-Proof NZlt_0_1.
-
-Theorem le_0_1 : 0 <= 1.
-Proof NZle_0_1.
-
-Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m.
-Proof NZlt_lt_succ_r.
-
-Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m.
-Proof NZle_le_succ_r.
-
-Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m.
-Proof NZle_succ_r.
-
-Theorem neq_succ_diag_l : forall n : N, S n ~= n.
-Proof NZneq_succ_diag_l.
-
-Theorem neq_succ_diag_r : forall n : N, n ~= S n.
-Proof NZneq_succ_diag_r.
-
-Theorem nlt_succ_diag_l : forall n : N, ~ S n < n.
-Proof NZnlt_succ_diag_l.
-
-Theorem nle_succ_diag_l : forall n : N, ~ S n <= n.
-Proof NZnle_succ_diag_l.
-
-Theorem le_succ_l : forall n m : N, S n <= m <-> n < m.
-Proof NZle_succ_l.
-
-Theorem lt_succ_l : forall n m : N, S n < m -> n < m.
-Proof NZlt_succ_l.
-
-Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m.
-Proof NZsucc_lt_mono.
-
-Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m.
-Proof NZsucc_le_mono.
-
-Theorem lt_asymm : forall n m : N, n < m -> ~ m < n.
-Proof NZlt_asymm.
-
-Notation lt_ngt := lt_asymm (only parsing).
-
-Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p.
-Proof NZlt_trans.
-
-Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p.
-Proof NZle_trans.
-
-Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p.
-Proof NZle_lt_trans.
-
-Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p.
-Proof NZlt_le_trans.
-
-Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m.
-Proof NZle_antisymm.
-
-(** Trichotomy, decidability, and double negation elimination *)
-
-Theorem lt_trichotomy : forall n m : N,  n < m \/ n == m \/ m < n.
-Proof NZlt_trichotomy.
-
-Notation lt_eq_gt_cases := lt_trichotomy (only parsing).
-
-Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m.
-Proof NZlt_gt_cases.
-
-Theorem le_gt_cases : forall n m : N, n <= m \/ n > m.
-Proof NZle_gt_cases.
-
-Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m.
-Proof NZlt_ge_cases.
-
-Theorem le_ge_cases : forall n m : N, n <= m \/ n >= m.
-Proof NZle_ge_cases.
-
-Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m.
-Proof NZle_ngt.
-
-Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m.
-Proof NZnlt_ge.
-
-Theorem lt_dec : forall n m : N, decidable (n < m).
-Proof NZlt_dec.
-
-Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m.
-Proof NZlt_dne.
-
-Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m.
-Proof NZnle_gt.
-
-Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m.
-Proof NZlt_nge.
-
-Theorem le_dec : forall n m : N, decidable (n <= m).
-Proof NZle_dec.
-
-Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m.
-Proof NZle_dne.
-
-Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m.
-Proof NZnlt_succ_r.
-
-Theorem lt_exists_pred :
-  forall z n : N, z < n -> exists k : N, n == S k /\ z <= k.
-Proof NZlt_exists_pred.
-
-Theorem lt_succ_iter_r :
-  forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m.
-Proof NZlt_succ_iter_r.
-
-Theorem neq_succ_iter_l :
-  forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m.
-Proof NZneq_succ_iter_l.
-
-(** Stronger variant of induction with assumptions n >= 0 (n < 0)
-in the induction step *)
-
-Theorem right_induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N, A z ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-        forall n : N, z <= n -> A n.
-Proof NZright_induction.
-
-Theorem left_induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N, A z ->
-      (forall n : N, n < z -> A (S n) -> A n) ->
-        forall n : N, n <= z -> A n.
-Proof NZleft_induction.
-
-Theorem right_induction' :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-      (forall n : N, n <= z -> A n) ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-        forall n : N, A n.
-Proof NZright_induction'.
-
-Theorem left_induction' :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-    (forall n : N, z <= n -> A n) ->
-    (forall n : N, n < z -> A (S n) -> A n) ->
-      forall n : N, A n.
-Proof NZleft_induction'.
-
-Theorem strong_right_induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-    (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
-       forall n : N, z <= n -> A n.
-Proof NZstrong_right_induction.
-
-Theorem strong_left_induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-      (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
-        forall n : N, n <= z -> A n.
-Proof NZstrong_left_induction.
-
-Theorem strong_right_induction' :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-      (forall n : N, n <= z -> A n) ->
-      (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
-        forall n : N, A n.
-Proof NZstrong_right_induction'.
-
-Theorem strong_left_induction' :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N,
-    (forall n : N, z <= n -> A n) ->
-    (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
-      forall n : N, A n.
-Proof NZstrong_left_induction'.
-
-Theorem order_induction :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N, A z ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-      (forall n : N, n < z  -> A (S n) -> A n) ->
-        forall n : N, A n.
-Proof NZorder_induction.
-
-Theorem order_induction' :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall z : N, A z ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-      (forall n : N, n <= z -> A n -> A (P n)) ->
-        forall n : N, A n.
-Proof NZorder_induction'.
-
-(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and
-ZOrder) since they boil down to regular induction *)
-
-(** Elimintation principle for < *)
-
-Theorem lt_ind :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall n : N,
-      A (S n) ->
-      (forall m : N, n < m -> A m -> A (S m)) ->
-        forall m : N, n < m -> A m.
-Proof NZlt_ind.
-
-(** Elimintation principle for <= *)
-
-Theorem le_ind :
-  forall A : N -> Prop, Proper (Neq==>iff) A ->
-    forall n : N,
-      A n ->
-      (forall m : N, n <= m -> A m -> A (S m)) ->
-        forall m : N, n <= m -> A m.
-Proof NZle_ind.
-
-(** Well-founded relations *)
-
-Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m).
-Proof NZlt_wf.
-
-Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z).
-Proof NZgt_wf.
+(* Theorems that are true for natural numbers but not for integers *)
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m).
+setoid_replace lt with (fun n m => 0 <= n /\ n < m).
 apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
 Defined.
 
-(* Theorems that are true for natural numbers but not for integers *)
-
 (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
 
-Theorem nlt_0_r : forall n : N, ~ n < 0.
+Theorem nlt_0_r : forall n, ~ n < 0.
 Proof.
 intro n; apply -> le_ngt. apply le_0_l.
 Qed.
 
-Theorem nle_succ_0 : forall n : N, ~ (S n <= 0).
+Theorem nle_succ_0 : forall n, ~ (S n <= 0).
 Proof.
 intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r.
 Qed.
 
-Theorem le_0_r : forall n : N, n <= 0 <-> n == 0.
+Theorem le_0_r : forall n, n <= 0 <-> n == 0.
 Proof.
 intros n; split; intro H.
 le_elim H; [false_hyp H nlt_0_r | assumption].
 now apply eq_le_incl.
 Qed.
 
-Theorem lt_0_succ : forall n : N, 0 < S n.
+Theorem lt_0_succ : forall n, 0 < S n.
 Proof.
 induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r].
 Qed.
 
-Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n.
+Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
 Proof.
 cases n.
 split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
 intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
 Qed.
 
-Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n.
+Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n.
 Proof.
 cases n.
 now left.
 intro; right; apply lt_0_succ.
 Qed.
 
-Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n.
+Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n.
 Proof.
 induct n. now left.
 cases n. intros; right; now left.
@@ -365,7 +74,7 @@ right; right. rewrite H. apply lt_succ_diag_r.
 right; right. now apply lt_lt_succ_r.
 Qed.
 
-Theorem lt_1_r : forall n : N, n < 1 <-> n == 0.
+Theorem lt_1_r : forall n, n < 1 <-> n == 0.
 Proof.
 cases n.
 split; intro; [reflexivity | apply lt_succ_diag_r].
@@ -373,7 +82,7 @@ intros n. rewrite <- succ_lt_mono.
 split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0].
 Qed.
 
-Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1.
+Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1.
 Proof.
 cases n.
 split; intro; [now left | apply le_succ_diag_r].
@@ -381,31 +90,30 @@ intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd.
 split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]].
 Qed.
 
-Theorem lt_lt_0 : forall n m : N, n < m -> 0 < m.
+Theorem lt_lt_0 : forall n m, n < m -> 0 < m.
 Proof.
 intros n m; induct n.
 trivial.
 intros n IH H. apply IH; now apply lt_succ_l.
 Qed.
 
-Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p.
+Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p.
 Proof.
-intros n m p H1 H2.
-apply le_lt_trans with m. apply <- le_succ_l. apply le_lt_trans with n.
-apply le_0_l. assumption. assumption.
+intros. apply lt_1_l with m; auto.
+apply le_lt_trans with n; auto. now apply le_0_l.
 Qed.
 
 (** Elimination principlies for < and <= for relations *)
 
 Section RelElim.
 
-Variable R : relation N.
-Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
+Variable R : relation N.t.
+Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.
 
 Theorem le_ind_rel :
-   (forall m : N, R 0 m) ->
-   (forall n m : N, n <= m -> R n m -> R (S n) (S m)) ->
-     forall n m : N, n <= m -> R n m.
+   (forall m, R 0 m) ->
+   (forall n m, n <= m -> R n m -> R (S n) (S m)) ->
+     forall n m, n <= m -> R n m.
 Proof.
 intros Base Step; induct n.
 intros; apply Base.
@@ -416,9 +124,9 @@ intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto.
 Qed.
 
 Theorem lt_ind_rel :
-   (forall m : N, R 0 (S m)) ->
-   (forall n m : N, n < m -> R n m -> R (S n) (S m)) ->
-   forall n m : N, n < m -> R n m.
+   (forall m, R 0 (S m)) ->
+   (forall n m, n < m -> R n m -> R (S n) (S m)) ->
+   forall n m, n < m -> R n m.
 Proof.
 intros Base Step; induct n.
 intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]].
@@ -433,61 +141,64 @@ End RelElim.
 
 (** Predecessor and order *)
 
-Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n.
+Theorem succ_pred_pos : forall n, 0 < n -> S (P n) == n.
 Proof.
 intros n H; apply succ_pred; intro H1; rewrite H1 in H.
 false_hyp H lt_irrefl.
 Qed.
 
-Theorem le_pred_l : forall n : N, P n <= n.
+Theorem le_pred_l : forall n, P n <= n.
 Proof.
 cases n.
 rewrite pred_0; now apply eq_le_incl.
 intros; rewrite pred_succ;  apply le_succ_diag_r.
 Qed.
 
-Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
+Theorem lt_pred_l : forall n, n ~= 0 -> P n < n.
 Proof.
 cases n.
 intro H; exfalso; now apply H.
 intros; rewrite pred_succ;  apply lt_succ_diag_r.
 Qed.
 
-Theorem le_le_pred : forall n m : N, n <= m -> P n <= m.
+Theorem le_le_pred : forall n m, n <= m -> P n <= m.
 Proof.
 intros n m H; apply le_trans with n. apply le_pred_l. assumption.
 Qed.
 
-Theorem lt_lt_pred : forall n m : N, n < m -> P n < m.
+Theorem lt_lt_pred : forall n m, n < m -> P n < m.
 Proof.
 intros n m H; apply le_lt_trans with n. apply le_pred_l. assumption.
 Qed.
 
-Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *)
+Theorem lt_le_pred : forall n m, n < m -> n <= P m.
+ (* Converse is false for n == m == 0 *)
 Proof.
 intro n; cases m.
 intro H; false_hyp H nlt_0_r.
 intros m IH. rewrite pred_succ; now apply -> lt_succ_r.
 Qed.
 
-Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
+Theorem lt_pred_le : forall n m, P n < m -> n <= m.
+ (* Converse is false for n == m == 0 *)
 Proof.
 intros n m; cases n.
 rewrite pred_0; intro H; now apply lt_le_incl.
 intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l.
 Qed.
 
-Theorem lt_pred_lt : forall n m : N, n < P m -> n < m.
+Theorem lt_pred_lt : forall n m, n < P m -> n < m.
 Proof.
 intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l].
 Qed.
 
-Theorem le_pred_le : forall n m : N, n <= P m -> n <= m.
+Theorem le_pred_le : forall n m, n <= P m -> n <= m.
 Proof.
 intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l].
 Qed.
 
-Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *)
+Theorem pred_le_mono : forall n m, n <= m -> P n <= P m.
+ (* Converse is false for n == 1, m == 0 *)
 Proof.
 intros n m H; elim H using le_ind_rel.
 solve_relation_wd.
@@ -495,7 +206,7 @@ intro; rewrite pred_0; apply le_0_l.
 intros p q H1 _; now do 2 rewrite pred_succ.
 Qed.
 
-Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
+Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.
 assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
@@ -506,22 +217,24 @@ apply lt_le_trans with (P m). assumption. apply le_pred_l.
 apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2.
 Qed.
 
-Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
+Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
 Proof.
 intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ.
 Qed.
 
-Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
+Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m.
+ (* Converse is false for n == m == 0 *)
 Proof.
 intros n m H. apply lt_le_pred. now apply -> le_succ_l.
 Qed.
 
-Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *)
+Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m.
+ (* Converse is false for n == m == 0 *)
 Proof.
 intros n m H. apply <- lt_succ_r. now apply lt_pred_le.
 Qed.
 
-Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
+Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m.
 Proof.
 intros n m; cases n.
 rewrite pred_0. split; intro H; apply le_0_l.
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
new file mode 100644
index 0000000000..29bda136a1
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export NAxioms NSub.
+
+(** This functor summarizes all known facts about N.
+    For the moment it is only an alias to [NSubPropFunct], which
+    subsumes all others.
+*)
+
+Module NPropFunct := NSubPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 1f5392f4a9..fee9b4372e 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -15,15 +15,15 @@ and proves its properties *)
 
 Require Export NSub.
 
-Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NSubPropMod := NSubPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NStrongRecPropFunct (Import N : NAxiomsSig).
+Include NSubPropFunct N.
+Local Open Scope NumScope.
 
 Section StrongRecursion.
 
 Variable A : Type.
 Variable Aeq : relation A.
-Context (Aeq_equiv : Equivalence Aeq).
+Variable Aeq_equiv : Equivalence Aeq.
 
 (** [strong_rec] allows to define a recursive function [phi] given by
     an equation [phi(n) = F(phi)(n)] where recursive calls to [phi]
@@ -37,13 +37,13 @@ Context (Aeq_equiv : Equivalence Aeq).
       that coincide with [phi] for numbers strictly less than [n].
 *)
 
-Definition strong_rec (a : A) (f : (N -> A) -> N -> A) (n : N) : A :=
+Definition strong_rec (a : A) (f : (N.t -> A) -> N.t -> A) (n : N.t) : A :=
  recursion (fun _ => a) (fun _ => f) (S n) n.
 
 (** For convenience, we use in proofs an intermediate definition
     between [recursion] and [strong_rec]. *)
 
-Definition strong_rec0 (a : A) (f : (N -> A) -> N -> A) : N -> N -> A :=
+Definition strong_rec0 (a : A) (f : (N.t -> A) -> N.t -> A) : N.t -> N.t -> A :=
  recursion (fun _ => a) (fun _ => f).
 
 Lemma strong_rec_alt : forall a f n,
@@ -54,13 +54,13 @@ Qed.
 
 (** We need a result similar to [f_equal], but for setoid equalities. *)
 Lemma f_equiv : forall f g x y,
- (Neq==>Aeq)%signature f g -> Neq x y -> Aeq (f x) (g y).
+ (N.eq==>Aeq)%signature f g -> N.eq x y -> Aeq (f x) (g y).
 Proof.
 auto.
 Qed.
 
 Instance strong_rec0_wd :
- Proper (Aeq ==> ((Neq ==> Aeq) ==> Neq ==> Aeq) ==> Neq ==> Neq ==> Aeq)
+ Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq)
   strong_rec0.
 Proof.
 unfold strong_rec0.
@@ -70,7 +70,7 @@ apply recursion_wd; try red; auto.
 Qed.
 
 Instance strong_rec_wd :
- Proper (Aeq ==> ((Neq ==> Aeq) ==> Neq ==> Aeq) ==> Neq ==> Aeq) strong_rec.
+ Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
 rewrite !strong_rec_alt.
@@ -80,8 +80,8 @@ Qed.
 
 Section FixPoint.
 
-Variable f : (N -> A) -> N -> A.
-Context (f_wd : Proper ((Neq==>Aeq)==>Neq==>Aeq) f).
+Variable f : (N.t -> A) -> N.t -> A.
+Variable f_wd : Proper ((N.eq==>Aeq)==>N.eq==>Aeq) f.
 
 Lemma strong_rec0_0 : forall a m,
  (strong_rec0 a f 0 m) = a.
@@ -112,8 +112,8 @@ calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
 coincide on values < n, then (f h1 n) coincides with (f h2 n) *)
 
 Hypothesis step_good :
-  forall (n : N) (h1 h2 : N -> A),
-    (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f h1 n) (f h2 n).
+  forall (n : N.t) (h1 h2 : N.t -> A),
+    (forall m : N.t, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f h1 n) (f h2 n).
 
 Lemma strong_rec0_more_steps : forall a k n m, m < n ->
  Aeq (strong_rec0 a f n m) (strong_rec0 a f (n+k) m).
@@ -135,7 +135,7 @@ Proof.
  apply lt_le_trans with m; auto.
 Qed.
 
-Lemma strong_rec0_fixpoint : forall (a : A) (n : N),
+Lemma strong_rec0_fixpoint : forall (a : A) (n : N.t),
  Aeq (strong_rec0 a f (S n) n) (f (fun n => strong_rec0 a f (S n) n) n).
 Proof.
 intros.
@@ -152,7 +152,7 @@ apply sub_add.
 rewrite le_succ_l; auto.
 Qed.
 
-Theorem strong_rec_fixpoint : forall (a : A) (n : N),
+Theorem strong_rec_fixpoint : forall (a : A) (n : N.t),
  Aeq (strong_rec a f n) (f (strong_rec a f) n).
 Proof.
 intros.
@@ -168,7 +168,7 @@ Qed.
     that the first argument of [f] is arbitrary in this case...
 *)
 
-Theorem strong_rec_0_any : forall (a : A)(any : N->A),
+Theorem strong_rec_0_any : forall (a : A)(any : N.t->A),
  Aeq (strong_rec a f 0) (f any 0).
 Proof.
 intros.
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index cfeb6709b2..62d1c731cc 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -12,45 +12,30 @@
 
 Require Export NMulOrder.
 
-Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Module NSubPropFunct (Import N : NAxiomsSig).
+Include NMulOrderPropFunct N.
+Local Open Scope NumScope.
 
-Theorem sub_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2.
-Proof NZsub_wd.
-
-Theorem sub_0_r : forall n : N, n - 0 == n.
-Proof NZsub_0_r.
-
-Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m).
-Proof NZsub_succ_r.
-
-Theorem sub_1_r : forall n : N, n - 1 == P n.
-Proof.
-intro n; rewrite sub_succ_r; now rewrite sub_0_r.
-Qed.
-
-Theorem sub_0_l : forall n : N, 0 - n == 0.
+Theorem sub_0_l : forall n, 0 - n == 0.
 Proof.
 induct n.
 apply sub_0_r.
 intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0.
 Qed.
 
-Theorem sub_succ : forall n m : N, S n - S m == n - m.
+Theorem sub_succ : forall n m, S n - S m == n - m.
 Proof.
 intro n; induct m.
 rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ.
 intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r.
 Qed.
 
-Theorem sub_diag : forall n : N, n - n == 0.
+Theorem sub_diag : forall n, n - n == 0.
 Proof.
 induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH.
 Qed.
 
-Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0.
+Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
 Proof.
 intros n m H; elim H using lt_ind_rel; clear n m H.
 solve_relation_wd.
@@ -58,7 +43,7 @@ intro; rewrite sub_0_r; apply neq_succ_0.
 intros; now rewrite sub_succ.
 Qed.
 
-Theorem add_sub_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p.
+Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.
 Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite sub_0_r.
@@ -68,32 +53,32 @@ rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l).
 reflexivity.
 Qed.
 
-Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n).
+Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n).
 Proof.
 intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)).
 symmetry; now apply add_sub_assoc.
 Qed.
 
-Theorem add_sub : forall n m : N, (n + m) - m == n.
+Theorem add_sub : forall n m, (n + m) - m == n.
 Proof.
 intros n m. rewrite <- add_sub_assoc by (apply le_refl).
 rewrite sub_diag; now rewrite add_0_r.
 Qed.
 
-Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m.
+Theorem sub_add : forall n m, n <= m -> (m - n) + n == m.
 Proof.
 intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption.
 rewrite add_comm. apply add_sub.
 Qed.
 
-Theorem add_sub_eq_l : forall n m p : N, m + p == n -> n - m == p.
+Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
 Proof.
 intros n m p H. symmetry.
 assert (H1 : m + p - m == n - m) by now rewrite H.
 rewrite add_comm in H1. now rewrite add_sub in H1.
 Qed.
 
-Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m.
+Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
 Proof.
 intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l.
 Qed.
@@ -101,7 +86,7 @@ Qed.
 (* This could be proved by adding m to both sides. Then the proof would
 use add_sub_assoc and sub_0_le, which is proven below. *)
 
-Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
+Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n.
 Proof.
 intros n m p H; double_induct n m.
 intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H.
@@ -110,14 +95,14 @@ intros n m IH H1. rewrite sub_succ in H1. apply IH in H1.
 rewrite add_succ_l; now rewrite H1.
 Qed.
 
-Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p.
+Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
 Proof.
 intros n m; induct p.
 rewrite add_0_r; now rewrite sub_0_r.
 intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH.
 Qed.
 
-Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
+Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
 rewrite (add_comm n m).
@@ -127,7 +112,7 @@ Qed.
 
 (** Sub and order *)
 
-Theorem le_sub_l : forall n m : N, n - m <= n.
+Theorem le_sub_l : forall n m, n - m <= n.
 Proof.
 intro n; induct m.
 rewrite sub_0_r; now apply eq_le_incl.
@@ -135,7 +120,7 @@ intros m IH. rewrite sub_succ_r.
 apply le_trans with (n - m); [apply le_pred_l | assumption].
 Qed.
 
-Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m.
+Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.
 Proof.
 double_induct n m.
 intro m; split; intro; [apply le_0_l | apply sub_0_l].
@@ -146,7 +131,7 @@ Qed.
 
 (** Sub and mul *)
 
-Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n.
+Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
 Proof.
 intros n m; cases m.
 now rewrite pred_0, mul_0_r, sub_0_l.
@@ -155,7 +140,7 @@ now rewrite sub_diag, add_0_r.
 now apply eq_le_incl.
 Qed.
 
-Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
+Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
 Proof.
 intros n m p; induct n.
 now rewrite sub_0_l, mul_0_l, sub_0_l.
@@ -170,11 +155,72 @@ setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_l
 apply mul_0_l.
 Qed.
 
-Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
+Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m.
 Proof.
 intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).
 apply mul_sub_distr_r.
 Qed.
 
+(** Alternative definitions of [<=] and [<] based on [+] *)
+
+Definition le_alt n m := exists p, p + n == m.
+Definition lt_alt n m := exists p, S p + n == m.
+
+Lemma le_equiv : forall n m, le_alt n m <-> n <= m.
+Proof.
+split.
+intros (p,H). rewrite <- H, add_comm. apply le_add_r.
+intro H. exists (m-n). now apply sub_add.
+Qed.
+
+Lemma lt_equiv : forall n m, lt_alt n m <-> n < m.
+Proof.
+split.
+intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r.
+intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r.
+apply sub_add. now rewrite le_succ_l.
+Qed.
+
+Instance le_alt_wd : Proper (eq==>eq==>iff) le_alt.
+Proof.
+ intros x x' Hx y y' Hy; unfold le_alt.
+ setoid_rewrite Hx. setoid_rewrite Hy. auto with *.
+Qed.
+
+Instance lt_alt_wd : Proper (eq==>eq==>iff) lt_alt.
+Proof.
+ intros x x' Hx y y' Hy; unfold lt_alt.
+ setoid_rewrite Hx. setoid_rewrite Hy. auto with *.
+Qed.
+
+(** With these alternative definition, the dichotomy:
+
+[forall n m, n <= m \/ m <= n]
+
+becomes:
+
+[forall n m, (exists p, p + n == m) \/ (exists p, p + m == n)]
+
+We will need this in the proof of induction principle for integers
+constructed as pairs of natural numbers. This formula can be proved
+from know properties of [<=]. However, it can also be done directly. *)
+
+Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n.
+Proof.
+intros n m; induct n.
+left; exists m; apply add_0_r.
+intros n IH.
+destruct IH as [[p H] | [p H]].
+destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
+rewrite add_0_l in H. right; exists (S 0); rewrite H, add_succ_l;
+ now rewrite add_0_l.
+left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
+right; exists (S p). rewrite add_succ_l; now rewrite H.
+Qed.
+
+Theorem add_dichotomy :
+  forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
+Proof le_alt_dichotomy.
+
 End NSubPropFunct.