Added the directory theories/Numbers where axiomatizations and implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet.

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

14 files changed, 2265 insertions, 0 deletions

diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
new file mode 100644
index 000000000..55f07eb89
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -0,0 +1,333 @@
+Require Export NDomain.
+
+(*********************************************************************
+*                            Peano Axioms                            *
+*********************************************************************)
+
+Module Type NatSignature.
+Declare Module Export DomainModule : DomainSignature.
+
+Parameter Inline O : N.
+Parameter Inline S : N -> N.
+
+Notation "0" := O.
+Notation "1" := (S O).
+
+Add Morphism S with signature E ==> E as S_wd.
+
+(* It is natural to formulate induction for well-defined predicates
+only because standard induction
+forall P, P 0 -> (forall n, P n -> P (S n)) -> forall n, P n
+does not hold in the setoid context (for example, there is no reason
+for (P x) hold when x == 0 but x <> 0). However, it is possible to
+formulate induction without mentioning well-defidedness (see OtherInd.v);
+this formulation is equivalent. *)
+Axiom induction :
+  forall P : N -> Prop, pred_wd E P ->
+    P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n.
+
+(* Why do we separate induction and recursion?
+
+(1) When induction and recursion are the same, they are dependent
+(nondependent induction does not make sense). However, one must impose
+conditions on the predicate, or codomain, that it respects the setoid
+equality. For induction this means considering predicates P for which
+forall n n', n == n' -> (P n <-> P n') holds. For recursion, where P :
+nat -> Set, we cannot say (P n <-> P n'). It may make sense to require
+forall n n', n == n' -> (P n = P n').
+
+(2) Unlike induction, recursion requires that two equalities hold:
+[recursion a f 0 == a] and [recursion a f (S n) == f n (recursion a f n)]
+(or something like this). It may be difficult to state, let alone prove,
+these equalities because the left- and the right-hand sides may have
+different types (P t1) and (P t2) where t1 == t2 is provable but t1 and t2
+are not convertible into each other. Nevertheless, these equalities may
+be proved using dependent equality (EqdepFacts) or JM equality (JMeq).
+However, requiring this for any implementation of natural numbers seems
+a little complex. It may make sense to devote a separate module to dependent
+recursion (see DepRec.v). *)
+
+Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A.
+
+Implicit Arguments recursion [A].
+
+(* Suppose the codomain A has a setoid equality relation EA. If A is a
+function space C -> D, it makes sense to consider extensional
+functional equality as EA. Indeed, suppose, for example, that we say
+[Definition g (x : N) : C -> D := (recursion ... x ...)]. We would
+like to show that the function g of two arguments is well-defined.
+This requirement is the same as the requirement that the functions of
+one argument (g x) and (g x') are extensionally equal whenever x ==
+x', i.e.,
+
+forall x x' : N, x == x' -> eq_fun (g x) (g x'),
+
+which is the same as
+
+forall x x' : N, x == x' -> forall y y' : C, EC y y' -> ED (g x y) (g x' y')
+
+where EC and ED are setoid equalities on C and D, respectively.
+
+Now, if we consider EA to be extensional equality on the function
+space, we cannot require that EA is reflexive. Indeed, reflexivity of
+EA:
+
+forall f : C -> D, eq_fun f f
+
+or
+
+forall f : C -> D, forall x x', EC x x' -> ED (f x) (f x')
+
+means that every function f ; C -> D is well-defined, which is in
+general false. We can expect that EA is symmetric and transitive,
+i.e., that EA is a partial equivalence relation (PER). However, there
+seems to be no need to require this in the following axioms.
+
+When we defined a function by recursion, the arguments of this
+function may occur in the recursion's base case a, the counter x, or
+the step function f. For example, in the following definition:
+
+Definition plus (x y : N) := recursion y (fun _ p => S p) x.
+
+one argument becomes the base case and the other becomes the counter.
+
+In the definitions of times:
+
+Definition times (x y : N) := recursion 0 (fun x p => plus y p) x.
+
+the argument y occurs in the step function. Thus it makes sense to
+formulate an axiom saying that (recursion a f x) is equal to
+(recursion a' f' x') whenever (EA a a'), x == x', and eq_fun2 f f'. We
+need to vary all three arguments; for example, claiming that
+(recursion a f x) equals (recursion a' f x') with the same f whenever
+(EA a a') and x == x' is not enough to prove well-defidedness of
+multiplication defined above.
+
+This leads to the axioms given below. There is a question if it is
+possible to formulate simpler axioms that would imply this statement
+for any implementation. Indeed, the proof seems to have to proceed by
+straighforward induction on x. The difficulty is that we cannot prove
+(EA (recursion a f x) (recursion a' f' x')) using the induction axioms
+above because recursion is not declared to be a setoid morphism:
+that's what we are proving! Therefore, this has to be proved by
+induction inside each particular implementation. *)
+
+Axiom recursion_wd : forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+
+(* Can we instead declare recursion as a morphism? It does not seem
+so. For this, we need to register the relation EA, and for this we
+need to declare it as a variable in a section. But information about
+morhisms is lost when sections are closed. *)
+
+(* When the function recursion is polymorphic on the codomain A, there
+seems no other option than to return the given base case a when the
+counter is 0. Therefore, we can formulate the following axioms with
+Leibniz equality. *)
+
+Axiom recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+
+Axiom recursion_S :
+  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+
+(* It may be possible to formulate recursion_0 and recursion_S as follows:
+Axiom recursion_0 :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a.
+
+Axiom recursion_S :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
+
+Then it is possible to prove recursion_wd (see IotherInd.v). This
+raises some questions:
+
+(1) Can the axioms recursion_wd, recursion_0 and recursion_S (both
+variants) proved for all reasonable implementations?
+
+(2) Can these axioms be proved without assuming that EA is symmetric
+and transitive? In OtherInd.v, recursion_wd can be proved from
+recursion_0 and recursion_S by assuming symmetry and transitivity.
+
+(2) Which variant requires proving less for each implementation? Can
+it be that proving all three axioms about recursion has some common
+parts which have to be repeated? *)
+
+Implicit Arguments recursion_wd [A].
+Implicit Arguments recursion_0 [A].
+Implicit Arguments recursion_S [A].
+
+End NatSignature.
+
+Module NatProperties (Export NatModule : NatSignature).
+
+Module Export  DomainPropertiesModule := DomainProperties DomainModule.
+
+(* This tactic applies the induction axioms and solves the resulting
+goal "pred_wd E P" *)
+Ltac induct n :=
+  try intros until n;
+  pattern n; apply induction; clear n;
+  [unfold NumPrelude.pred_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | |].
+
+Definition if_zero (A : Set) (a b : A) (n : N) : A :=
+  recursion a (fun _ _ => b) n.
+
+Add Morphism if_zero with signature LE_Set ==> LE_Set ==> E ==> LE_Set as if_zero_wd.
+Proof.
+unfold LE_Set.
+intros; unfold if_zero; now apply recursion_wd with (EA := (@eq A));
+[| unfold eq_fun2; now intros |].
+Qed.
+
+Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
+Proof.
+unfold if_zero; intros; now rewrite recursion_0.
+Qed.
+
+Theorem if_zero_S : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
+Proof.
+intros; unfold if_zero.
+now rewrite (recursion_S (@eq A)); [| | unfold fun2_wd; now intros].
+Qed.
+
+Implicit Arguments if_zero [A].
+
+(* To prove this statement, we need to provably different terms,
+e.g., true and false *)
+Theorem S_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_S.
+pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0.
+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.
+Qed.
+
+Theorem not_eq_S : forall n m, n # m -> S n # S m.
+Proof.
+intros n m H1 H2. apply S_inj in H2. now apply H1.
+Qed.
+
+Theorem not_eq_Sn_n : forall n, S n # n.
+Proof.
+induct n.
+apply S_0.
+intros n IH H. apply S_inj in H. now apply IH.
+Qed.
+
+Theorem not_all_eq_0 : ~ forall n, n == 0.
+Proof.
+intro H; apply (S_0 0). apply H.
+Qed.
+
+Theorem not_0_implies_S : forall n, n # 0 <-> exists m, n == S m.
+Proof.
+intro n; split.
+induct n; [intro H; now elim H | intros n _ _; now exists n].
+intro H; destruct H as [m H]; rewrite H; apply S_0.
+Qed.
+
+Theorem nondep_induction :
+  forall P : N -> Prop, NumPrelude.pred_wd E P ->
+    P 0 -> (forall n, P (S n)) -> forall n, P n.
+Proof.
+intros; apply induction; auto.
+Qed.
+
+Ltac nondep_induct n :=
+  try intros until n;
+  pattern n; apply nondep_induction; clear n;
+  [unfold NumPrelude.pred_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | |].
+
+Theorem O_or_S : forall n, n == 0 \/ exists m, n == S m.
+Proof.
+nondep_induct n; [now left | intros n; right; now exists n].
+Qed.
+
+(* The following is useful for reasoning about, e.g., Fibonacci numbers *)
+Section DoubleInduction.
+Variable P : N -> Prop.
+Hypothesis P_correct : NumPrelude.pred_wd E P.
+
+Add Morphism P with signature E ==> iff as P_morphism.
+Proof.
+exact P_correct.
+Qed.
+
+Theorem double_induction :
+  P 0 -> P 1 ->
+    (forall n, P n -> P (S n) -> P (S (S n))) -> forall n, P n.
+Proof.
+intros until 3.
+assert (D : forall n, P n /\ P (S n)); [ |intro n; exact (proj1 (D n))].
+induct n; [ | intros n [IH1 IH2]]; auto.
+Qed.
+
+End DoubleInduction.
+
+(* The following is useful for reasoning about, e.g., Ackermann function *)
+Section TwoDimensionalInduction.
+Variable R : N -> N -> Prop.
+Hypothesis R_correct : rel_wd E R.
+
+Add Morphism R with signature E ==> E ==> iff as R_morphism.
+Proof.
+exact R_correct.
+Qed.
+
+Theorem two_dim_induction :
+   R 0 0 ->
+   (forall n m, R n m -> R n (S m)) ->
+   (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m.
+Proof.
+intros H1 H2 H3. induct n.
+induct m.
+exact H1. exact (H2 0).
+intros n IH. induct m.
+now apply H3. exact (H2 (S n)).
+Qed.
+
+End TwoDimensionalInduction.
+
+End NatProperties.
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
new file mode 100644
index 000000000..7da105f5b
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -0,0 +1,71 @@
+Require Import NAxioms.
+Require Import NPlus.
+Require Import NTimes.
+
+(* Here we allow dependent recursion only for domains with Libniz
+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 DomainModule : DomainEqSignature.
+Declare Module Export NatModule : NatSignature with
+  Module DomainModule := DomainModule.
+(* Instead of these two lines, I would like to say
+Declare Module Export Nat : NatSignature with Module Domain : NatDomainEq. *)
+
+Parameter Inline dep_recursion :
+  forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
+
+Axiom dep_recursion_0 :
+  forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)),
+    dep_recursion A a f 0 = a.
+
+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.
+
+Module DepRecTimesProperties (Export DepRecModule : DepRecSignature)
+                             (Export TimesModule : TimesSignature
+                                with Module PlusModule.NatModule := DepRecModule.NatModule).
+
+Module Export TimesPropertiesModule := TimesProperties TimesModule.
+
+Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}.
+Proof.
+intro n; pattern n; apply dep_recursion; clear n;
+[intro H; now elim H | intros n _ _; now exists n].
+Qed.
+
+Theorem plus_eq_1_dep :
+  forall m n : N, m + n == 1 -> {m == 0 /\ n == 1} + {m == 1 /\ n == 0}.
+(* Why do we write == here instead of just = ? "x == y" is a notation
+for (E x y) declared (along with E := (@eq N)) in NatDomainEq signature. If we
+want to rewrite, e.g., plus_comm, which contains E, in a formula with
+=, setoid rewrite signals an error, because E is not declared a
+morphism w.r.t. = even though E is defined to be =. Thus, we need to
+use E instead of = in our formulas. *)
+Proof.
+intros m n; pattern m; apply dep_recursion; clear m.
+intro H.
+rewrite plus_0_n in H. left; now split.
+intros m IH H. rewrite plus_Sn_m in H. apply S_inj in H.
+apply plus_eq_0 in H. destruct H as [H1 H2].
+right; now split; [rewrite H1 |].
+Qed.
+
+Theorem times_eq_0_dep :
+  forall n m, n * m == 0 -> {n == 0} + {m == 0}.
+Proof.
+intros n m; pattern n; apply dep_recursion; pattern m; apply dep_recursion;
+clear n m.
+intros; left; reflexivity.
+intros; left; reflexivity.
+intros; right; reflexivity.
+intros n _ m _ H.
+rewrite times_Sn_m in H; rewrite plus_Sn_m in H; now apply S_0 in H.
+Qed.
+
+End DepRecTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
new file mode 100644
index 000000000..ebc692d5b
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -0,0 +1,77 @@
+Require Export NumPrelude.
+
+Module Type DomainSignature.
+
+Parameter Inline N : Set.
+Parameter Inline E : relation N.
+Parameter Inline e : N -> N -> bool.
+
+(* Theoretically, we it is enough to have decidable equality e only.
+If necessary, E could be defined using a coercion. However, after we
+prove properties of natural numbers, we would like them to eventually
+use ordinary Leibniz equality. E.g., we would like the commutativity
+theorem, instantiated to nat, to say forall x y : nat, x + y = y + x,
+and not forall x y : nat, eq_true (e (x + y) (y + x))
+
+In fact, if we wanted to have decidable equality e only, we would have
+some trouble doing rewriting. If there is a hypothesis H : e x y, this
+means more precisely that H : eq_true (e x y). Such hypothesis is not
+recognized as equality by setoid rewrite because it does not have the
+form R x y where R is an identifier. *)
+
+Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
+Axiom E_equiv : equiv N E.
+
+Add Relation N E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+Notation "x # y" := (~ E x y) (at level 70).
+
+End DomainSignature.
+
+(* Now we give DomainSignature, but with E being Leibniz equality. If
+an implementation uses this signature, then more facts may be proved
+about it. *)
+Module Type DomainEqSignature.
+
+Parameter Inline N : Set.
+Definition E := (@eq N).
+Parameter Inline e : N -> N -> bool.
+
+Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
+Definition E_equiv : equiv N E := eq_equiv N.
+
+Add Relation N E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+Notation "x # y" := ((E x y) -> False) (at level 70).
+(* Why do we need a new notation for Leibniz equality? See DepRec.v *)
+
+End DomainEqSignature.
+
+Module DomainProperties (Export DomainModule : DomainSignature).
+(* It also accepts module of type NatDomainEq *)
+
+(* The following easily follows from transitivity of e and E, but
+we need to deal with the coercion *)
+Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
+Proof.
+intros x x' Exx' y y' Eyy'.
+case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
+assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
+assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
+rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
+assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
+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.
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v
new file mode 100644
index 000000000..41d7d6145
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NIso.v
@@ -0,0 +1,115 @@
+Require Import 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 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).
+
+Definition homomorphism (f : N1 -> N2) : Prop :=
+  f O1 == O2 /\ forall x : N1, f (S1 x) == S2 (f x).
+
+Definition natural_isomorphism : N1 -> N2 :=
+  Nat1.recursion O2 (fun (x : N1) (p : N2) => S2 p).
+
+Add Morphism natural_isomorphism
+with signature E1 ==> E2
+as natural_isomorphism_wd.
+Proof.
+unfold natural_isomorphism.
+intros x y Exy.
+apply Nat1.recursion_wd with (EA := E2).
+reflexivity.
+unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.S_wd.
+assumption.
+Qed.
+
+Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2.
+Proof.
+unfold natural_isomorphism; now rewrite Nat1.recursion_0.
+Qed.
+
+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);
+[| unfold fun2_wd; intros; apply Nat2.S_wd |].
+Qed.
+
+Theorem iso_hom : homomorphism natural_isomorphism.
+Proof.
+unfold homomorphism, natural_isomorphism; split;
+[exact natural_isomorphism_0 | exact natural_isomorphism_S].
+Qed.
+
+End Homomorphism.
+
+Module Inverse (Nat1 Nat2 : NatSignature).
+
+Module Import NatProperties1 := NatProperties Nat1.
+(* This makes the tactic induct available. Since it is taken from
+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 h12 := Hom12.natural_isomorphism.
+Notation Local h21 := Hom21.natural_isomorphism.
+
+Notation Local "x == y" := (Nat1.DomainModule.E x y) (at level 70).
+
+Lemma iso_inverse :
+  forall x : N1, h21 (h12 x) == x.
+Proof.
+induct x.
+now rewrite Hom12.natural_isomorphism_0; rewrite Hom21.natural_isomorphism_0.
+intros x IH.
+rewrite Hom12.natural_isomorphism_S; rewrite Hom21.natural_isomorphism_S;
+now rewrite IH.
+Qed.
+
+End Inverse.
+
+Module Isomorphism (Nat1 Nat2 : NatSignature).
+
+Module Hom12 := Homomorphism Nat1 Nat2.
+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 h12 := Hom12.natural_isomorphism.
+Notation Local h21 := Hom21.natural_isomorphism.
+
+Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop :=
+  Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
+  forall x : N1, E1 (f2 (f1 x)) x /\
+  forall y : N2, E2 (f1 (f2 y)) y.
+
+Theorem iso_iso : isomorphism h12 h21.
+Proof.
+unfold isomorphism.
+split. apply Hom12.iso_hom.
+split. apply Hom21.iso_hom.
+split. apply Inverse121.iso_inverse.
+apply Inverse212.iso_inverse.
+Qed.
+
+End Isomorphism.
diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v
new file mode 100644
index 000000000..210786bba
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NLt.v
@@ -0,0 +1,168 @@
+Require Export NAxioms.
+
+Module Type LtSignature.
+Declare Module Export NatModule : NatSignature.
+
+Parameter Inline lt : N -> N -> bool.
+
+Notation "x < y" := (lt x y).
+
+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.
+
+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/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
new file mode 100644
index 000000000..5f9b7b1d1
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -0,0 +1,373 @@
+Require Import Bool. (* To get the negb function *)
+Require Import NAxioms.
+Require Import NStrongRec.
+Require Import NPlus.
+Require Import NTimes.
+Require Import NLt.
+Require Import NPlusLt.
+Require Import NTimesLt.
+
+Module MiscFunctFunctor (NatMod : NatSignature).
+Module Export NatPropertiesModule := NatProperties NatMod.
+Module Export StrongRecPropertiesModule := StrongRecProperties NatMod.
+
+(*****************************************************)
+(**                   Addition                       *)
+
+Definition plus (x y : N) := recursion y (fun _ p => S p) x.
+
+Lemma plus_step_wd : fun2_wd E E E (fun _ p => S p).
+Proof.
+unfold fun2_wd; intros _ _ _ p p' H; now rewrite H.
+Qed.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+unfold plus.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (EA := E).
+assumption.
+unfold eq_fun2; intros _ _ _ p p' Epp'; now rewrite Epp'.
+assumption.
+Qed.
+
+Theorem plus_0 : forall y, plus 0 y == y.
+Proof.
+intro y. unfold plus.
+(*pose proof (recursion_0 E y (fun _ p => S p)) as H.*)
+rewrite recursion_0. apply (proj1 E_equiv).
+Qed.
+
+Theorem plus_S : forall x y, plus (S x) y == S (plus x y).
+Proof.
+intros x y; unfold plus.
+now rewrite (recursion_S E); [|apply plus_step_wd|].
+Qed.
+
+(*****************************************************)
+(**                  Multiplication                  *)
+
+Definition times (x y : N) := recursion 0 (fun x p => plus y p) x.
+
+Lemma times_step_wd : forall y, fun2_wd E E E (fun x p => plus y p).
+Proof.
+unfold fun2_wd. intros y _ _ _ p p' Ezz'.
+now apply plus_wd.
+Qed.
+
+Lemma times_step_equal :
+  forall y y', y == y' -> eq_fun2 E E E (fun x p => plus y p) (fun x p => plus y' p).
+Proof.
+unfold eq_fun2; intros; apply plus_wd; assumption.
+Qed.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+unfold times.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (EA := E).
+reflexivity. apply times_step_equal. assumption. assumption.
+Qed.
+
+Theorem times_0 : forall y, times 0 y == 0.
+Proof.
+intro y. unfold times. now rewrite recursion_0.
+Qed.
+
+Theorem times_S : forall x y, times (S x) y == plus y (times x y).
+Proof.
+intros x y; unfold times.
+now rewrite (recursion_S E); [| apply times_step_wd |].
+Qed.
+
+(*****************************************************)
+(**                   Less Than                      *)
+
+Definition lt (m : N) : N -> bool :=
+  recursion (if_zero false true)
+            (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+            m.
+
+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.
+
+Lemma lt_step_wd :
+  let step := (fun _ f => fun n => recursion false (fun n' _ => f n') n) in
+    eq_fun2 E (eq_fun E eq_bool) (eq_fun E eq_bool) step step.
+Proof.
+unfold eq_fun2, eq_fun, eq_bool.
+intros x x' Exx' f f' Eff' y y' Eyy'.
+apply recursion_wd with (EA := eq_bool); unfold eq_bool.
+reflexivity.
+unfold eq_fun2; intros; now apply Eff'.
+assumption.
+Qed.
+
+Lemma lt_curry_wd : forall m m', m == m' -> eq_fun E eq_bool (lt m) (lt m').
+Proof.
+unfold lt.
+intros m m' Emm'.
+apply recursion_wd with (EA := eq_fun E eq_bool).
+apply lt_base_wd.
+apply lt_step_wd.
+assumption.
+Qed.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold eq_fun; intros m m' Emm' n n' Enn'.
+now apply lt_curry_wd.
+Qed.
+
+(* Note that if we unfold lt along with eq_fun above, then "apply" signals
+as error "Impossible to unify", not just, e.g., "Cannot solve second-order
+unification problem". Something is probably wrong. *)
+
+Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n.
+Proof.
+intro n; unfold lt; now rewrite recursion_0.
+Qed.
+
+Theorem lt_step_eq : forall m n, lt (S m) n = recursion false (fun n' _ => lt m n') n.
+Proof.
+intros m n; unfold lt.
+pose proof (recursion_S (eq_fun E eq_bool) (if_zero false true)
+  (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+  lt_base_wd lt_step_wd m n n) as H.
+unfold eq_bool in H.
+assert (H1 : n == n); [reflexivity | apply H in H1; now rewrite H1].
+Qed.
+
+Theorem lt_0 : forall n, ~ lt n 0.
+Proof.
+nondep_induct n.
+rewrite lt_base_eq; rewrite if_zero_0; now intro.
+intros n; rewrite lt_step_eq. rewrite recursion_0. now intro.
+Qed.
+
+(* Above, we rewrite applications of function. Is it possible to rewrite
+functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
+lt_step n (recursion lt_base lt_step n)? *)
+
+Lemma lt_0_1 : lt 0 1.
+Proof.
+rewrite lt_base_eq; now rewrite if_zero_S.
+Qed.
+
+Lemma lt_0_Sn : forall n, lt 0 (S n).
+Proof.
+intro n; rewrite lt_base_eq; now rewrite if_zero_S.
+Qed.
+
+Lemma lt_Sn_Sm : forall n m, lt (S n) (S m) <-> lt n m.
+Proof.
+intros n m.
+rewrite lt_step_eq. rewrite (recursion_S eq_bool).
+reflexivity.
+now unfold eq_bool.
+unfold fun2_wd; intros; now apply lt_wd.
+Qed.
+
+Theorem lt_S : forall m n, lt m (S n) <-> lt m n \/ m == n.
+Proof.
+induct m.
+nondep_induct n;
+[split; intro; [now right | apply lt_0_1] |
+intro n; split; intro; [left |]; apply lt_0_Sn].
+intros n IH. nondep_induct n0.
+split.
+intro. assert (H1 : lt n 0); [now apply -> lt_Sn_Sm | false_hyp H1 lt_0].
+intro H; destruct H as [H | H].
+false_hyp H lt_0. false_hyp H S_0.
+intro m. pose proof (IH m) as H; clear IH.
+assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_Sn_Sm |].
+assert (lt (S n) (S m) <-> lt n m); [apply lt_Sn_Sm |].
+assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|].
+tauto.
+Qed.
+
+(*****************************************************)
+(**                     Even                         *)
+
+Definition even (x : N) := recursion true (fun _ p => negb p) x.
+
+Lemma even_step_wd : fun2_wd E eq_bool eq_bool (fun x p => if p then false else true).
+Proof.
+unfold fun2_wd.
+intros x x' Exx' b b' Ebb'.
+unfold eq_bool; destruct b; destruct b'; now simpl.
+Qed.
+
+Add Morphism even with signature E ==> eq_bool as even_wd.
+Proof.
+unfold even; intros.
+apply recursion_wd with (A := bool) (EA := eq_bool).
+now unfold eq_bool.
+unfold eq_fun2. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
+assumption.
+Qed.
+
+Theorem even_0 : even 0 = true.
+Proof.
+unfold even.
+now rewrite recursion_0.
+Qed.
+
+Theorem even_S : forall x : N, even (S x) = negb (even x).
+Proof.
+unfold even.
+intro x; rewrite (recursion_S (@eq bool)); try reflexivity.
+unfold fun2_wd.
+intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
+Qed.
+
+(*****************************************************)
+(**                Division by 2                     *)
+
+Definition half_aux (x : N) : N * N :=
+  recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
+
+Definition half (x : N) := snd (half_aux x).
+
+Definition E2 := prod_rel E E.
+
+Add Relation (prod N N) E2
+reflexivity proved by (prod_rel_refl N N E E E_equiv E_equiv)
+symmetry proved by (prod_rel_symm N N E E E_equiv E_equiv)
+transitivity proved by (prod_rel_trans N N E E E_equiv E_equiv)
+as E2_rel.
+
+Lemma half_step_wd: fun2_wd E E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
+Proof.
+unfold fun2_wd, E2, prod_rel.
+intros _ _ _ p1 p2 [H1 H2].
+destruct p1; destruct p2; simpl in *.
+now split; [rewrite H2 |].
+Qed.
+
+Add Morphism half with signature E ==> E as half_wd.
+Proof.
+unfold half.
+assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
+intros x y Exy; unfold half_aux; apply recursion_wd with (EA := E2); unfold E2.
+unfold E2.
+unfold prod_rel; simpl; now split.
+unfold eq_fun2, prod_rel; simpl.
+intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
+intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
+unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
+exact (proj2 Exy).
+Qed.
+
+(*****************************************************)
+(**            Logarithm for the base 2              *)
+
+Definition log (x : N) : N :=
+strong_rec 0
+           (fun x g =>
+              if (e x 0) then 0
+              else if (e x 1) then 0
+              else S (g (half x)))
+           x.
+
+Add Morphism log with signature E ==> E as log_wd.
+Proof.
+intros x x' Exx'. unfold log.
+apply strong_rec_wd with (EA := E); try (reflexivity || assumption).
+unfold eq_fun2. intros y y' Eyy' g g' Egg'.
+assert (H : e y 0 = e y' 0); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : e y 1 = e y' 1); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : S (g (half y)) == S (g' (half y')));
+[apply S_wd; apply Egg'; now apply half_wd|].
+now destruct (e y 0); destruct (e y 1).
+Qed.
+
+(*********************************************************)
+(** To get the properties of plus, times and lt defined  *)
+(** via recursion, we form the corresponding modules and *)
+(** apply the properties functors to these modules       *)
+
+Module DefaultPlusModule <: PlusSignature.
+
+Module NatModule := NatMod.
+(* If we used the name NatModule instead of NatMod then this would
+produce many warnings like "Trying to mask the absolute name
+NatModule", "Trying to mask the absolute name Nat.O" etc. *)
+
+Definition plus := plus.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+exact plus_wd.
+Qed.
+
+Theorem plus_0_n : forall n, plus 0 n == n.
+Proof.
+exact plus_0.
+Qed.
+
+Theorem plus_Sn_m : forall n m, plus (S n) m == S (plus n m).
+Proof.
+exact plus_S.
+Qed.
+
+End DefaultPlusModule.
+
+Module DefaultTimesModule <: TimesSignature.
+Module Export PlusModule := DefaultPlusModule.
+
+Definition times := times.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+exact times_wd.
+Qed.
+
+Theorem times_0_n : forall n, times 0 n == 0.
+Proof.
+exact times_0.
+Qed.
+
+Theorem times_Sn_m : forall n m, times (S n) m == plus m (times n m).
+Proof.
+exact times_S.
+Qed.
+
+End DefaultTimesModule.
+
+Module DefaultLtModule <: LtSignature.
+Module NatModule := NatMod.
+
+Definition lt := lt.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+exact lt_wd.
+Qed.
+
+Theorem lt_0 : forall x, ~ (lt x 0).
+Proof.
+exact lt_0.
+Qed.
+
+Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x == y.
+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.
+
+(*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).*)
+
+End MiscFunctFunctor.
diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v
new file mode 100644
index 000000000..e37669bad
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NOtherInd.v
@@ -0,0 +1,159 @@
+Require Export NDomain.
+Declare Module Export DomainModule : DomainSignature.
+
+Parameter O : N.
+Parameter S : N -> N.
+
+Notation "0" := O.
+
+Definition induction :=
+forall P : N -> Prop, pred_wd E P ->
+    P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n.
+
+Definition other_induction :=
+forall P : N -> Prop,
+  (forall n : N, n == 0 -> P n) ->
+  (forall n : N, P n -> forall m : N, m == S n -> P m) ->
+  forall n : N, P n.
+
+Theorem other_ind_implies_ind : other_induction -> induction.
+Proof.
+unfold induction, other_induction; intros OI P P_wd Base Step.
+apply OI; unfold pred_wd in P_wd.
+intros; now apply -> (P_wd 0).
+intros n Pn m EmSn; now apply -> (P_wd (S n)); [apply Step|].
+Qed.
+
+Theorem ind_implies_other_ind : induction -> other_induction.
+Proof.
+intros I P Base Step.
+set (Q := fun n => forall m, m == n -> P m).
+cut (forall n, Q n).
+unfold Q; intros H n; now apply (H n).
+apply I.
+unfold pred_wd, Q. intros x y Exy.
+split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy].
+exact Base.
+intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |].
+Qed.
+
+(* This theorem is not really needed. It shows that if we have
+other_induction and we proved the base case and the induction step, we
+can in fact show that the predicate in question is well-defined, and
+therefore we can turn this other induction into the standard one. *)
+Theorem other_ind_implies_pred_wd :
+other_induction ->
+  forall P : N -> Prop,
+    (forall n : N, n == 0 -> P n) ->
+    (forall n : N, P n -> forall m : N, m == S n -> P m) ->
+    pred_wd E P.
+Proof.
+intros OI P Base Step; unfold pred_wd.
+intros x; pattern x; apply OI; clear x.
+(* Base case *)
+intros x H1 y H2.
+assert (y == 0); [rewrite <- H2; now rewrite H1|].
+assert (P x); [now apply Base|].
+assert (P y); [now apply Base|].
+split; now intro.
+(* Step *)
+intros x IH z H y H1.
+rewrite H in H1. symmetry in H1.
+split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI.
+Qed.
+
+Section Recursion.
+
+Variable A : Set.
+Variable EA : relation A.
+Hypothesis EA_symm : symmetric A EA.
+Hypothesis EA_trans : transitive A EA.
+
+Add Relation A EA
+ symmetry proved by EA_symm
+ transitivity proved by EA_trans
+as EA_rel.
+
+Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a.
+Proof.
+intros a a' EAaa'.
+apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption].
+Qed.
+
+Parameter recursion : A -> (N -> A -> A) -> N -> A.
+
+Axiom recursion_0 :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a.
+
+Axiom recursion_S :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
+
+Theorem recursion_wd : induction ->
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+intros I a a' Eaa' f f' f_wd f'_wd Eff'.
+apply ind_implies_other_ind in I.
+intro x; pattern x; apply I; clear x.
+intros x Ex0 x' Exx'.
+rewrite Ex0 in Exx'; symmetry in Exx'.
+(* apply recursion_0 in Ex0. produces
+Anomaly: type_of: this is not a well-typed term. Please report. *)
+assert (EA (recursion a f x) a).
+apply recursion_0. now apply EA_neighbor with (a' := a'). assumption.
+assert (EA a' (recursion a' f' x')).
+apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption.
+apply EA_trans with (y := a). assumption.
+now apply EA_trans with (y := a').
+intros x IH y H y' H1.
+rewrite H in H1; symmetry in H1.
+assert (EA (recursion a f y) (f x (recursion a f x))).
+apply recursion_S. now apply EA_neighbor with (a' := a').
+assumption. now symmetry.
+assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')).
+symmetry; apply recursion_S. now apply EA_neighbor with (a' := a). assumption.
+now symmetry.
+assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))).
+apply Eff'. reflexivity. apply IH. reflexivity.
+apply EA_trans with (y := (f x (recursion a f x))). assumption.
+apply EA_trans with (y := (f' x (recursion a' f' x))). assumption.
+assumption.
+Qed.
+
+Axiom recursion_0' :
+  forall (a : A) (f : N -> A -> A),
+    forall x : N, x == 0 -> recursion a f x = a.
+
+Axiom recursion_S' :
+  forall (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
+
+Theorem recursion_wd' : other_induction ->
+  forall a a' : A, EA a a -> EA a' a' -> EA a a' ->
+    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'.
+intro x; pattern x; apply I; clear x.
+intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'.
+replace (recursion a f x) with a. replace (recursion a' f' x') with a'.
+assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'.
+intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'.
+apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_S'.
+apply EA_trans with (y := (f' x (recursion a' f' x))).
+apply Eff'. reflexivity. now apply IH.
+symmetry; now apply recursion_S'.
+Qed.
+
+
+
+End Recursion.
+
+Implicit Arguments recursion [A].
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
new file mode 100644
index 000000000..29b65e3f4
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -0,0 +1,184 @@
+Require Export NAxioms.
+
+Module Type PlusSignature.
+Declare Module Export NatModule : NatSignature.
+
+Parameter Inline plus : N -> N -> N.
+
+Notation "x + y" := (plus x y).
+
+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.
+
+Module PlusProperties (Export PlusModule : PlusSignature).
+
+Module Export NatPropertiesModule := NatProperties NatModule.
+
+Lemma plus_0_r : forall n, n + 0 == n.
+Proof.
+induct n.
+now rewrite plus_0_n.
+intros x IH.
+rewrite plus_Sn_m.
+now rewrite IH.
+Qed.
+
+Lemma plus_0_l : forall n, 0 + n == n.
+Proof.
+intro n.
+now rewrite plus_0_n.
+Qed.
+
+Lemma plus_n_Sm : forall n m, n + S m == S (n + m).
+Proof.
+intros n m; generalize n; clear n. induct n.
+now repeat rewrite plus_0_n.
+intros x IH.
+repeat rewrite plus_Sn_m; now rewrite IH.
+Qed.
+
+Lemma plus_Sn_m : forall n m, S n + m == S (n + m).
+Proof.
+intros.
+now rewrite plus_Sn_m.
+Qed.
+
+Lemma plus_comm : forall n m, n + m == m + n.
+Proof.
+intros n m; generalize n; clear n. induct n.
+rewrite plus_0_l; now rewrite plus_0_r.
+intros x IH.
+rewrite plus_Sn_m; rewrite plus_n_Sm; now rewrite IH.
+Qed.
+
+Lemma plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
+Proof.
+intros n m p; generalize n; clear n. induct n.
+now repeat rewrite plus_0_l.
+intros x IH.
+repeat rewrite plus_Sn_m; now rewrite IH.
+Qed.
+
+Lemma plus_1_l : forall n, 1 + n == S n.
+Proof.
+intro n; rewrite plus_Sn_m; now rewrite plus_0_n.
+Qed.
+
+Lemma plus_1_r : forall n, n + 1 == S n.
+Proof.
+intro n; rewrite plus_comm; apply plus_1_l.
+Qed.
+
+Lemma plus_cancel_l : forall n m p, p + n == p + m -> n == m.
+Proof.
+induct p.
+do 2 rewrite plus_0_n; trivial.
+intros p IH H. do 2 rewrite plus_Sn_m in H. apply S_inj in H. now apply IH.
+Qed.
+
+Lemma plus_cancel_r : forall n m p, n + p == m + p -> n == m.
+Proof.
+intros n m p.
+rewrite plus_comm.
+set (k := p + n); rewrite plus_comm; unfold k.
+apply plus_cancel_l.
+Qed.
+
+Lemma plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0.
+Proof.
+intros n m; induct n.
+rewrite plus_0_n; now split.
+intros n IH H. rewrite plus_Sn_m in H.
+absurd_hyp H; [|assumption]. unfold not; apply S_0.
+Qed.
+
+Lemma succ_plus_discr : forall n m, m # S (n + m).
+Proof.
+intro n; induct m.
+intro H. apply S_0 with (n := (n + 0)). now apply (proj2 (proj2 E_equiv)). (* symmetry *)
+intros m IH H. apply S_inj in H. rewrite plus_n_Sm in H.
+unfold not in IH; now apply IH.
+Qed.
+
+Lemma n_SSn : forall n, n # S (S n).
+Proof.
+intro n. pose proof (succ_plus_discr 1 n) as H.
+rewrite plus_Sn_m in H; now rewrite plus_0_n in H.
+Qed.
+
+Lemma n_SSSn : forall n, n # S (S (S n)).
+Proof.
+intro n. pose proof (succ_plus_discr (S (S 0)) n) as H.
+do 2 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
+Qed.
+
+Lemma n_SSSSn : forall n, n # S (S (S (S n))).
+Proof.
+intro n. pose proof (succ_plus_discr (S (S (S 0))) n) as H.
+do 3 rewrite plus_Sn_m in H. now rewrite plus_0_n in H.
+Qed.
+
+(* The following section is devoted to defining a function that, given
+two numbers whose some equals 1, decides which number equals 1. The
+main property of the function is also proved .*)
+
+(* First prove a theorem with ordinary disjunction *)
+Theorem plus_eq_1 :
+  forall m n, m + n == 1 ->  (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0).
+induct m.
+intros n H; rewrite plus_0_n in H; left; now split.
+intros n IH m H; rewrite plus_Sn_m in H; apply S_inj in H;
+apply plus_eq_0 in H; destruct H as [H1 H2];
+now right; split; [apply S_wd |].
+Qed.
+
+Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m.
+
+Lemma plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false).
+Proof.
+unfold fun2_wd; intros. unfold eq_bool. reflexivity.
+Qed.
+
+Add Morphism plus_eq_1_dec with signature E ==> E ==> eq_bool as plus_eq_1_dec_wd.
+Proof.
+unfold fun2_wd, plus_eq_1_dec.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (EA := eq_bool).
+unfold eq_bool; reflexivity.
+unfold eq_fun2; unfold eq_bool; reflexivity.
+assumption.
+Qed.
+
+Lemma plus_eq_1_dec_0 : forall n, plus_eq_1_dec 0 n = true.
+Proof.
+intro n. unfold plus_eq_1_dec.
+now apply recursion_0.
+Qed.
+
+Lemma plus_eq_1_dec_S : forall m n, plus_eq_1_dec (S n) m = false.
+Proof.
+intros n m. unfold plus_eq_1_dec.
+now rewrite (recursion_S eq_bool);
+[| unfold eq_bool | apply plus_eq_1_dec_step_wd].
+Qed.
+
+Theorem plus_eq_1_dec_correct :
+  forall m n, m + n == 1 ->
+    (plus_eq_1_dec m n = true  -> m == 0 /\ n == 1) /\
+    (plus_eq_1_dec m n = false -> m == 1 /\ n == 0).
+Proof.
+intros m n; induct m.
+intro H. rewrite plus_0_l in H.
+rewrite plus_eq_1_dec_0.
+split; [intros; now split | intro H1; discriminate H1].
+intros m _ H. rewrite plus_eq_1_dec_S.
+split; [intro H1; discriminate | intros _ ].
+rewrite plus_Sn_m in H. apply S_inj in H.
+apply plus_eq_0 in H; split; [apply S_wd | ]; tauto.
+Qed.
+
+End PlusProperties.
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v
new file mode 100644
index 000000000..ac322a8f2
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NPlusLt.v
@@ -0,0 +1,50 @@
+Require Export NPlus.
+Require Export NLt.
+
+Module PlusLtProperties (Export PlusModule : PlusSignature)
+                        (Export LtModule : LtSignature with
+                           Module NatModule := PlusModule.NatModule).
+
+Module Export PlusPropertiesModule := PlusProperties PlusModule.
+Module Export LtPropertiesModule := LtProperties LtModule.
+
+(* Print All locks up here !!! *)
+Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
+Proof.
+intros n m p; induct p.
+now rewrite plus_0_r.
+intros x IH H.
+rewrite plus_n_Sm. apply lt_closed_S. apply IH; apply H.
+Qed.
+
+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.
+Qed.
+
+Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
+Proof.
+intros n m p H; rewrite plus_comm.
+set (k := p + n); rewrite plus_comm; unfold k; clear k.
+now apply plus_lt_compat_l.
+Qed.
+
+Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply lt_transitive with (m := m + p);
+[now apply plus_lt_compat_r | now apply plus_lt_compat_l].
+Qed.
+
+Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
+Proof.
+intros n m p; induct p.
+now do 2 rewrite plus_0_n.
+intros x IH H.
+do 2 rewrite plus_Sn_m in H.
+apply IH; now apply -> S_respects_lt.
+Qed.
+
+End PlusLtProperties.
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v
new file mode 100644
index 000000000..a97dca9a5
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NStrongRec.v
@@ -0,0 +1,67 @@
+Require Import NAxioms.
+
+Module StrongRecProperties (Export NatModule : NatSignature).
+Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule.
+
+Section StrongRecursion.
+
+Variable A : Set.
+Variable EA : relation A.
+
+Hypothesis EA_equiv : equiv A EA.
+
+Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A :=
+(recursion (fun _ : N => a)
+           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
+           (S x)) x.
+
+Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A,
+fun2_wd E (eq_fun E EA) EA f ->
+  fun2_wd E (eq_fun E EA) (eq_fun E EA)
+    (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)).
+Proof.
+unfold fun2_wd; intros f f_wd.
+intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'.
+assert (H : e y x = e y' x'). now apply e_wd. rewrite H.
+destruct (e y' x'); simpl.
+now apply f_wd. now apply Egg'.
+Qed.
+
+Theorem strong_rec_wd :
+forall a a', EA a a' ->
+  forall f f', eq_fun2 E (eq_fun E EA) EA f f' ->
+    forall x x', x == x' ->
+      EA (strong_rec a f x) (strong_rec a' f' x').
+Proof.
+intros a a' Eaa' f f' Eff' x x' Exx'.
+assert (H : eq_fun E EA
+  (recursion (fun _ : N => a)
+           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
+           (S x))
+  (recursion (fun _ : N => a')
+           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y))
+           (S x'))).
+apply recursion_wd with (EA := eq_fun E EA).
+unfold eq_fun; now intros.
+unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'.
+assert (H: e z y = e z' y'); [now apply e_wd|].
+rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp'].
+now rewrite Exx'.
+unfold strong_rec.
+now apply H.
+Qed.
+
+(* To do:
+Definition step_good (g : N -> (N -> A) -> A) :=
+  forall (x : N) (h1 h2 : N -> A),
+    (forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2).
+
+Theorem strong_recursion_fixpoint : forall a g, step_good g ->
+  let f x := (strong_rec a g x) in forall x, EA (f x) (g x f).
+*)
+
+End StrongRecursion.
+
+Implicit Arguments strong_rec [A].
+
+End StrongRecProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
new file mode 100644
index 000000000..a47070083
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -0,0 +1,162 @@
+Require Export NPlus.
+
+Module Type TimesSignature.
+Declare Module Export PlusModule : PlusSignature.
+
+Parameter Inline times : N -> N -> N.
+
+Notation "x * y" := (times x y).
+
+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.
+
+Module TimesProperties (Export TimesModule : TimesSignature).
+
+Module Export PlusPropertiesModule := PlusProperties PlusModule.
+
+Theorem mult_0_r : forall n, n * 0 == 0.
+Proof.
+induct n.
+now rewrite times_0_n.
+intros x IH.
+rewrite times_Sn_m; now rewrite plus_0_n.
+Qed.
+
+Theorem mult_0_l : forall n, 0 * n == 0.
+Proof.
+intro n; now rewrite times_0_n.
+Qed.
+
+Theorem mult_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p.
+Proof.
+intros n m p; induct n.
+rewrite mult_0_l.
+now do 2 rewrite plus_0_l.
+intros x IH.
+rewrite plus_Sn_m.
+do 2 rewrite times_Sn_m.
+rewrite IH.
+apply plus_assoc.
+Qed.
+
+Theorem mult_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p.
+Proof.
+intros n m p; induct n.
+do 3 rewrite mult_0_l; now rewrite plus_0_l.
+intros x IH.
+do 3 rewrite times_Sn_m.
+rewrite IH.
+(* Now we have to rearrange the sum of 4 terms *)
+rewrite <- (plus_assoc m p (x * m + x * p)).
+rewrite (plus_assoc p (x * m) (x * p)).
+rewrite (plus_comm p (x * m)).
+rewrite <- (plus_assoc (x * m) p (x * p)).
+apply (plus_assoc m (x * m) (p + x * p)).
+Qed.
+
+Theorem mult_assoc : forall n m p, n * (m * p) == (n * m) * p.
+Proof.
+intros n m p; induct n.
+now do 3 rewrite mult_0_l.
+intros x IH.
+do 2 rewrite times_Sn_m.
+rewrite mult_plus_distr_r.
+now rewrite IH.
+Qed.
+
+Theorem mult_1_l : forall n, 1 * n == n.
+Proof.
+intro n.
+rewrite times_Sn_m; rewrite times_0_n. now rewrite plus_0_r.
+Qed.
+
+Theorem mult_1_r : forall n, n * 1 == n.
+Proof.
+induct n.
+now rewrite times_0_n.
+intros x IH.
+rewrite times_Sn_m; rewrite IH; rewrite plus_Sn_m; now rewrite plus_0_n.
+Qed.
+
+Theorem mult_comm : forall n m, n * m == m * n.
+Proof.
+intros n m.
+induct n.
+rewrite mult_0_l; now rewrite mult_0_r.
+intros x IH.
+rewrite times_Sn_m.
+assert (H : S x == S 0 + x).
+rewrite plus_Sn_m; rewrite plus_0_n; reflexivity.
+rewrite H.
+rewrite mult_plus_distr_l.
+rewrite mult_1_r; rewrite IH; reflexivity.
+Qed.
+
+Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0.
+Proof.
+induct n; induct m.
+intros; now left.
+intros; now left.
+intros; now right.
+intros m IH H1.
+rewrite times_Sn_m in H1; rewrite plus_Sn_m in H1; now apply S_0 in H1.
+Qed.
+
+Definition times_eq_0_dec (n m : N) : bool :=
+  recursion true (fun _ _ => recursion false (fun _ _ => false) m) n.
+
+Lemma times_eq_0_dec_wd_step :
+  forall y y', y == y' ->
+    eq_bool (recursion false (fun _ _ => false) y)
+            (recursion false (fun _ _ => false) y').
+Proof.
+intros y y' Eyy'.
+apply recursion_wd with (EA := eq_bool).
+now unfold eq_bool.
+unfold eq_fun2. intros. now unfold eq_bool.
+assumption.
+Qed.
+
+Add Morphism times_eq_0_dec with signature E ==> E ==> eq_bool
+as times_eq_0_dec_wd.
+unfold fun2_wd, times_eq_0_dec.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (EA := eq_bool).
+now unfold eq_bool.
+unfold eq_fun2; intros. now apply times_eq_0_dec_wd_step.
+assumption.
+Qed.
+
+Theorem times_eq_0_dec_correct :
+  forall n m, n * m == 0 ->
+    (times_eq_0_dec n m = true ->  n == 0) /\
+    (times_eq_0_dec n m = false -> m == 0).
+Proof.
+nondep_induct n; nondep_induct m; unfold times_eq_0_dec.
+rewrite recursion_0; split; now intros.
+intro n; rewrite recursion_0; split; now intros.
+intro; rewrite recursion_0; rewrite (recursion_S eq_bool);
+[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros].
+intro m; rewrite (recursion_S eq_bool).
+rewrite times_Sn_m. rewrite plus_Sn_m. intro H; now apply S_0 in H.
+now unfold eq_bool.
+unfold fun2_wd; intros; now unfold eq_bool.
+Qed.
+
+Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1.
+Proof.
+nondep_induct n; nondep_induct m.
+intro H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
+intros n H; rewrite times_0_n in H; symmetry in H; now apply S_0 in H.
+intro H; rewrite mult_0_r in H; symmetry in H; now apply S_0 in H.
+intros m H; rewrite times_Sn_m in H; rewrite plus_Sn_m in H;
+apply S_inj in H; rewrite mult_comm in H; rewrite times_Sn_m in H;
+apply plus_eq_0 in H; destruct H as [H1 H2];
+apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split.
+Qed.
+
+End TimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v
new file mode 100644
index 000000000..e67b5bb2a
--- /dev/null
+++ b/theories/Numbers/Natural/Axioms/NTimesLt.v
@@ -0,0 +1,64 @@
+Require Export NLt.
+Require Export NTimes.
+Require Export NPlusLt.
+
+Module TimesLtProperties (Export TimesModule : TimesSignature)
+                         (Export LtModule : LtSignature with
+                            Module NatModule := TimesModule.PlusModule.NatModule).
+
+Module Export TimesPropertiesModule := TimesProperties TimesModule.
+Module Export LtPropertiesModule := LtProperties LtModule.
+Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule.
+
+Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Proof.
+intros n m p; induct n.
+now do 2 rewrite mult_1_l.
+intros x IH H.
+rewrite times_Sn_m.
+set (k := S x * m); rewrite times_Sn_m; unfold k; clear k.
+apply plus_lt_compat; [assumption | apply IH; assumption].
+Qed.
+
+Lemma mult_S_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n).
+Proof.
+intros n m p H.
+set (k := (p * (S n))); rewrite mult_comm; unfold k; clear k.
+set (k := ((S n) * m)); rewrite mult_comm; unfold k; clear k.
+now apply mult_S_lt_compat_l.
+Qed.
+
+Lemma mult_lt_compat_l : forall m n p, n < m -> 0 < p -> p * n < p * m.
+Proof.
+intros n m p H1 H2.
+apply (lt_exists_pred p) in H2.
+destruct H2 as [q H]. repeat rewrite H.
+now apply mult_S_lt_compat_l.
+Qed.
+
+Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
+Proof.
+intros n m p H1 H2.
+apply (lt_exists_pred p) in H2.
+destruct H2 as [q H]. repeat rewrite H.
+now apply mult_S_lt_compat_r.
+Qed.
+
+Lemma mult_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m.
+Proof.
+intros n m H1 H2.
+rewrite <- (times_0_n m); now apply mult_lt_compat_r.
+Qed.
+
+Lemma mult_lt_compat : forall n m p q, n < m -> p < q -> n * p < m * q.
+Proof.
+intros n m p q; induct n.
+intros; rewrite times_0_n; apply mult_positive;
+[assumption | apply lt_positive with (n := p); assumption].
+intros x IH H1 H2.
+apply lt_transitive with (m := ((S x) * q)).
+now apply mult_S_lt_compat_l; assumption.
+now apply mult_lt_compat_r; [| apply lt_positive with (n := p)].
+Qed.
+
+End TimesLtProperties.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
new file mode 100644
index 000000000..47b39bfeb
--- /dev/null
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -0,0 +1,221 @@
+Require Import NArith.
+Require Import Ndec.
+
+Require Import NDepRec.
+Require Import NAxioms.
+Require Import NPlus.
+Require Import NTimes.
+Require Import NLt.
+Require Import NPlusLt.
+Require Import NTimesLt.
+Require Import NMiscFunct.
+
+Open Scope N_scope.
+
+Module BinaryDomain <: DomainEqSignature.
+
+Definition N := N.
+Definition E := (@eq N).
+Definition e := Neqb.
+
+Theorem E_equiv_e : forall x y : N, E x y <-> e x y.
+Proof.
+unfold E, e; intros x y; split; intro H;
+[rewrite H; now rewrite Neqb_correct |
+apply Neqb_complete; now inversion H].
+Qed.
+
+Definition E_equiv : equiv N E := eq_equiv N.
+
+Add Relation N E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+End BinaryDomain.
+
+Module BinaryNat <: NatSignature.
+
+Module Export DomainModule := BinaryDomain.
+
+Definition O := N0.
+Definition S := Nsucc.
+
+Add Morphism S with signature E ==> E as S_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem induction :
+  forall P : N -> Prop, pred_wd E P ->
+    P 0 -> (forall n, P n -> P (S n)) -> forall n, P n.
+Proof.
+intros P P_wd; apply Nind.
+Qed.
+
+Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
+  Nrec (fun _ => A) a f n.
+Implicit Arguments recursion [A].
+
+Theorem recursion_wd :
+forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
+      forall x x' : N, x = x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+unfold fun2_wd, E, eq_fun2.
+intros A EA a a' Eaa' f f' Eff'.
+intro x; pattern x; apply Nind.
+intros x' H; now rewrite <- H.
+clear x.
+intros x IH x' H; rewrite <- H.
+unfold recursion, Nrec in *; do 2 rewrite Nrect_step.
+now apply Eff'; [| apply IH].
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+Proof.
+intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base.
+Qed.
+
+Theorem recursion_S :
+  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+Proof.
+unfold E, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind.
+rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
+clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
+now rewrite Nrect_step.
+Qed.
+
+End BinaryNat.
+
+Module BinaryDepRec <: DepRecSignature.
+Module Export DomainModule := BinaryDomain.
+Module Export NatModule := BinaryNat.
+
+Definition dep_recursion := Nrec.
+
+Theorem dep_recursion_0 :
+  forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)),
+    dep_recursion A a f 0 = a.
+Proof.
+intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base.
+Qed.
+
+Theorem 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).
+Proof.
+intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step.
+Qed.
+
+End BinaryDepRec.
+
+Module BinaryPlus <: PlusSignature.
+
+Module Export NatModule := BinaryNat.
+
+Definition plus := Nplus.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem plus_0_n : forall n, 0 + n = n.
+Proof.
+exact Nplus_0_l.
+Qed.
+
+Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m).
+Proof.
+exact Nplus_succ.
+Qed.
+
+End BinaryPlus.
+
+Module BinaryTimes <: TimesSignature.
+Module Export PlusModule := BinaryPlus.
+
+Definition times := Nmult.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem times_0_n : forall n, 0 * n = 0.
+Proof.
+exact Nmult_0_l.
+Qed.
+
+Theorem times_Sn_m : forall n m, (S n) * m = m + n * m.
+Proof.
+exact Nmult_Sn_m.
+Qed.
+
+End BinaryTimes.
+
+Module BinaryLt <: LtSignature.
+Module Export NatModule := BinaryNat.
+
+Definition lt (m n : N) := less_than (Ncompare m n).
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem lt_0 : forall x, ~ (lt x 0).
+Proof.
+unfold lt; destruct x as [|x]; simpl; now intro.
+Qed.
+
+Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y.
+Proof.
+intros x y.
+assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt);
+[unfold lt, less_than; destruct (x ?= S y); simpl; split; now intro |].
+assert (H2 : lt x y <-> Ncompare x y = Lt);
+[unfold lt, less_than; destruct (x ?= y); simpl; split; now intro |].
+pose proof (Ncompare_n_Sm x y) as H. tauto.
+Qed.
+
+End BinaryLt.
+
+Module Export BinaryPlusProperties := PlusProperties BinaryPlus.
+Module Export BinaryTimesProperties := TimesProperties BinaryTimes.
+Module Export BinaryDepRecTimesProperties :=
+  DepRecTimesProperties BinaryDepRec BinaryTimes.
+Module Export BinaryLtProperties := LtProperties BinaryLt.
+Module Export BinaryPlusLtProperties := PlusLtProperties BinaryPlus BinaryLt.
+Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt.
+
+Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.
+(* Time Eval compute in (log 100000). *) (* 98 sec *)
+
+Fixpoint binposlog (p : positive) : N :=
+match p with
+| xH => 0
+| xO p' => Nsucc (binposlog p')
+| xI p' => Nsucc (binposlog p')
+end.
+
+Definition binlog (n : N) : N :=
+match n with
+| 0 => 0
+| Npos p => binposlog p
+end.
+
+(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
+
+
+(*Check nat_total_order : forall n m : N, (n = m -> False) -> lt n m \/ lt m n.
+Check mult_positive : forall n m : N, lt 0 n -> lt 0 m -> lt 0 (n * m).*)
+
+Close Scope N_scope.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
new file mode 100644
index 000000000..403521e7c
--- /dev/null
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -0,0 +1,221 @@
+Require Import NDepRec.
+Require Import NPlus.
+Require Import NTimes.
+Require Import NLt.
+Require Import NPlusLt.
+Require Import NTimesLt.
+Require Import NMiscFunct.
+
+Module PeanoDomain <: DomainEqSignature.
+
+Definition N := nat.
+Definition E := (@eq nat).
+Definition e := eq_nat_bool.
+
+Theorem E_equiv_e : forall x y : N, E x y <-> e x y.
+Proof.
+unfold E, e; intros x y; split; intro H;
+[rewrite H; apply eq_nat_bool_refl |
+now apply eq_nat_bool_implies_eq].
+Qed.
+
+Definition E_equiv : equiv N E := eq_equiv N.
+
+Add Relation N E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+End PeanoDomain.
+
+Module PeanoNat <: NatSignature.
+
+Module Export DomainModule := PeanoDomain.
+
+Definition O := 0.
+Definition S := S.
+
+Add Morphism S with signature E ==> E as S_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem induction :
+  forall P : nat -> Prop, pred_wd (@eq nat) P ->
+    P 0 -> (forall n, P n -> P (S n)) -> forall n, P n.
+Proof.
+intros P W Base Step n; elim n; assumption.
+Qed.
+
+Definition recursion := fun A : Set => nat_rec (fun _ => A).
+Implicit Arguments recursion [A].
+
+Theorem recursion_wd :
+forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
+      forall x x' : N, x = x' ->
+        EA (recursion a f x) (recursion a' f' x').
+Proof.
+unfold fun2_wd, E.
+intros A EA a a' Eaa' f f' Eff'.
+induction x as [| n IH]; intros x' H; rewrite <- H; simpl.
+assumption.
+apply Eff'; [reflexivity | now apply IH].
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a.
+Proof.
+reflexivity.
+Qed.
+
+Theorem recursion_S :
+forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+  EA a a -> fun2_wd E EA EA f ->
+    forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+Proof.
+intros A EA a f EAaa f_wd. unfold fun2_wd, E in *.
+induction n; simpl; now apply f_wd.
+Qed.
+
+End PeanoNat.
+
+Module PeanoDepRec <: DepRecSignature.
+
+Module Export DomainModule := PeanoDomain.
+Module Export NatModule <: NatSignature := PeanoNat.
+
+Definition dep_recursion := nat_rec.
+
+Theorem dep_recursion_0 :
+  forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)),
+    dep_recursion A a f 0 = a.
+Proof.
+reflexivity.
+Qed.
+
+Theorem 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).
+Proof.
+reflexivity.
+Qed.
+
+End PeanoDepRec.
+
+Module PeanoPlus <: PlusSignature.
+
+Module Export NatModule := PeanoNat.
+
+Definition plus := plus.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem plus_0_n : forall n, 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem plus_Sn_m : forall n m, (S n) + m = S (n + m).
+Proof.
+reflexivity.
+Qed.
+
+End PeanoPlus.
+
+Module PeanoTimes <: TimesSignature.
+Module Export PlusModule := PeanoPlus.
+
+Definition times := mult.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem times_0_n : forall n, 0 * n = 0.
+Proof.
+auto.
+Qed.
+
+Theorem times_Sn_m : forall n m, (S n) * m = m + n * m.
+Proof.
+auto.
+Qed.
+
+End PeanoTimes.
+
+(* Some checks:
+Check times_eq_1 : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Eval compute in times_eq_0_dec 0 5.
+Eval compute in times_eq_0_dec 5 0. *)
+
+Module PeanoLt <: LtSignature.
+Module Export NatModule := PeanoNat.
+
+Definition lt := lt_bool.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold E, eq_bool; congruence.
+Qed.
+
+Theorem lt_0 : forall x, ~ (lt x 0).
+Proof.
+exact lt_bool_0.
+Qed.
+
+Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y.
+Proof.
+exact lt_bool_S.
+Qed.
+
+End PeanoLt.
+
+(* Obtaining properties for +, *, <, and their combinations *)
+
+Module Export PeanoPlusProperties := PlusProperties PeanoPlus.
+Module Export PeanoTimesProperties := TimesProperties PeanoTimes.
+Module Export PeanoLtProperties := LtProperties PeanoLt.
+Module Export PeanoPlusLtProperties := PlusLtProperties PeanoPlus PeanoLt.
+Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt.
+Module Export PeanoDepRecTimesProperties :=
+  DepRecTimesProperties PeanoDepRec PeanoTimes.
+
+Module MiscFunctModule := MiscFunctFunctor PeanoNat.
+
+(*Eval compute in MiscFunctModule.lt 6 5.*)
+
+(*Set Printing All.*)
+(*Check plus_comm.
+Goal forall x y : nat, x + y = y + x.
+intros x y.
+rewrite plus_comm. reflexivity. (* does now work -- but the next line does *)
+apply plus_comm.*)
+
+(*Opaque plus.
+Eval compute in (forall n m : N, E m (PeanoPlus.Nat.S (PeanoPlus.plus n m)) -> False).
+
+Eval compute in (plus_eq_1_dec 1 1).
+Opaque plus_eq_1_dec.
+Check plus_eq_1.
+Eval compute in (forall m n : N,
+       E (PeanoPlus.plus m n) (PeanoPlus.Nat.S PeanoPlus.Nat.O) ->
+       (plus_eq_1_dec m n = true ->
+        E m PeanoPlus.Nat.O /\ E n (PeanoPlus.Nat.S PeanoPlus.Nat.O)) /\
+       (plus_eq_1_dec m n = false ->
+        E m (PeanoPlus.Nat.S PeanoPlus.Nat.O) /\ E n PeanoPlus.Nat.O)).*)
+
+(*Require Import rec_ex.
+
+Module Import PeanoRecursionExamples := RecursionExamples PeanoNat.
+
+Eval compute in mult 3 15.
+Eval compute in e 100 100.
+Eval compute in log 8.
+Eval compute in half 0.*)