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

24 files changed, 4037 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
new file mode 100644
index 000000000..4f0eab8e3
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZAxioms.v
@@ -0,0 +1,120 @@
+Require Import NumPrelude.
+Require Import ZDomain.
+
+Module Type IntSignature.
+Declare Module Export DomainModule : DomainSignature.
+
+Parameter Inline O : Z.
+Parameter Inline S : Z -> Z.
+Parameter Inline P : Z -> Z.
+
+Notation "0" := O.
+
+Add Morphism S with signature E ==> E as S_wd.
+Add Morphism P with signature E ==> E as P_wd.
+
+Axiom S_inj : forall x y : Z, S x == S y -> x == y.
+Axiom S_P : forall x : Z, S (P x) == x.
+
+Axiom induction :
+  forall Q : Z -> Prop,
+    pred_wd E Q -> Q 0 ->
+    (forall x, Q x -> Q (S x)) ->
+    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+
+End IntSignature.
+
+
+Module IntProperties (Export IntModule : IntSignature).
+
+Module Export DomainPropertiesModule := DomainProperties DomainModule.
+
+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 | | |].
+
+Theorem P_inj : forall x y, P x == P y -> x == y.
+Proof.
+intros x y H.
+setoid_replace x with (S (P x)); [| symmetry; apply S_P].
+setoid_replace y with (S (P y)); [| symmetry; apply S_P].
+now rewrite H.
+Qed.
+
+Theorem P_S : forall x, P (S x) == x.
+Proof.
+intro x.
+apply S_inj.
+now rewrite S_P.
+Qed.
+
+(* The following tactics are intended for replacing a certain
+occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
+Unfortunately, this cannot be done by setoid_replace tactic for two
+reasons. First, it seems impossible to do rewriting when one side of
+the equation in question (S_P or P_S) is a variable, due to bug 1604.
+This does not work even when the predicate is an identifier (e.g.,
+when one tries to rewrite (Q x) into (Q (S (P x)))). Second, the
+setoid_rewrite tactic, like the ordinary rewrite tactic, does not
+allow specifying the exact occurrence of the term to be rewritten. Now
+while not in the setoid context, this occurrence can be specified
+using the pattern tactic, it does not work with setoids, since pattern
+creates a lambda abstractuion, and setoid_rewrite does not work with
+them. *)
+
+Ltac rewrite_SP t set_tac repl thm :=
+let x := fresh "x" in
+set_tac x t;
+setoid_replace x with (repl x); [| symmetry; apply thm];
+unfold x; clear x.
+
+Tactic Notation "rewrite_S_P" constr(t) :=
+rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P.
+
+Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) :=
+rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P.
+
+Tactic Notation "rewrite_P_S" constr(t) :=
+rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S.
+
+Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) :=
+rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S.
+
+(* One can add tactic notations for replacements in assumptions rather
+than in the goal. For the reason of many possible variants, the core
+of the tactic is factored out. *)
+
+Section Induction.
+
+Variable Q : Z -> Prop.
+Hypothesis Q_wd : pred_wd E Q.
+
+Add Morphism Q with signature E ==> iff as Q_morph.
+Proof Q_wd.
+
+Theorem induction_n :
+  forall n, Q n ->
+    (forall m, Q m -> Q (S m)) ->
+    (forall m, Q m -> Q (P m)) -> forall m, Q m.
+Proof.
+induct n.
+intros; now apply induction.
+intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1.
+intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1.
+Qed.
+
+End Induction.
+
+Ltac induct_n k n :=
+  try intros until k;
+  pattern k; apply induction_n with (n := n); clear k;
+  [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 | | |].
+
+End IntProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
new file mode 100644
index 000000000..00eab8842
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -0,0 +1,42 @@
+Require Import NumPrelude.
+
+Module Type DomainSignature.
+
+Parameter Z : Set.
+Parameter E : relation Z.
+Parameter e : Z -> Z -> bool.
+
+Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
+Axiom E_equiv : equiv Z E.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+Notation "x # y" := (~ E x y) (at level 70).
+
+End DomainSignature.
+
+Module DomainProperties (Export DomainModule : DomainSignature).
+
+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.
+
+Theorem neq_symm : forall n m, n # m -> m # n.
+Proof.
+intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+Qed.
+
+End DomainProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
new file mode 100644
index 000000000..b1983d6f7
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -0,0 +1,447 @@
+Require Import NumPrelude.
+Require Import ZDomain.
+Require Import ZAxioms.
+Require Import Coq.ZArith.Zmisc. (* for iter_nat *)
+
+Module Type OrderSignature.
+Declare Module Export IntModule : IntSignature.
+
+Parameter Inline lt : Z -> Z -> bool.
+Parameter Inline le : Z -> Z -> bool.
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+
+Notation "n <  m" := (lt n m).
+Notation "n <= m" := (le n m).
+
+Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m.
+Axiom lt_irr : forall n, ~ (n < n).
+Axiom lt_S : forall n m, n < (S m) <-> n <= m.
+
+End OrderSignature.
+
+
+Module OrderProperties (Export OrderModule : OrderSignature).
+Module Export IntPropertiesModule := IntProperties IntModule.
+
+Ltac le_intro1 := rewrite le_lt; left.
+Ltac le_intro2 := rewrite le_lt; right.
+Ltac le_elim H := rewrite le_lt in H; destruct H as [H | H].
+
+Theorem le_refl : forall n, n <= n.
+Proof.
+intro n; now le_intro2.
+Qed.
+
+Theorem lt_n_Sn : forall n, n < S n.
+Proof.
+intro n. rewrite lt_S. now le_intro2.
+Qed.
+
+Theorem le_n_Sn : forall n, n <= S n.
+Proof.
+intro; le_intro1; apply lt_n_Sn.
+Qed.
+
+Theorem lt_Pn_n : forall n, P n < n.
+Proof.
+intro n; rewrite_S_P n at 2; apply lt_n_Sn.
+Qed.
+
+Theorem le_Pn_n : forall n, P n <= n.
+Proof.
+intro; le_intro1; apply lt_Pn_n.
+Qed.
+
+Theorem lt_n_Sm : forall n m, n < m -> n < S m.
+Proof.
+intros. rewrite lt_S. now le_intro1.
+Qed.
+
+Theorem le_n_Sm : forall n m, n <= m -> n <= S m.
+Proof.
+intros n m H; rewrite <- lt_S in H; now le_intro1.
+Qed.
+
+Theorem lt_n_m_P : forall n m, n < m <-> n <= P m.
+Proof.
+intros n m; rewrite_S_P m; rewrite P_S; apply lt_S.
+Qed.
+
+Theorem not_le_n_Pn : forall n, ~ n <= P n.
+Proof.
+intros n H; le_elim H.
+apply lt_n_Sm in H; rewrite S_P in H; false_hyp H lt_irr.
+pose proof (lt_Pn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem le_S : forall n m, n <= S m <-> n <= m \/ n == S m.
+Proof.
+intros n m; rewrite le_lt. now rewrite lt_S.
+Qed.
+
+Theorem lt_P : forall n m, (P n) < m <-> n <= m.
+Proof.
+intro n; induct_n m (P n).
+split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn.
+intros m IH; split; intro H.
+apply -> lt_S in H; le_elim H.
+apply -> IH in H; now apply le_n_Sm.
+rewrite <- H; rewrite S_P; now le_intro2.
+apply -> le_S in H; destruct H as [H | H].
+apply <- IH in H. now apply lt_n_Sm. rewrite H; rewrite P_S; apply lt_n_Sn.
+intros m IH; split; intro H.
+pose proof H as H1. apply lt_n_Sm in H; rewrite S_P in H.
+apply -> IH in H; le_elim H. now apply -> lt_n_m_P.
+rewrite H in H1; false_hyp H1 lt_irr.
+pose proof H as H1. apply le_n_Sm in H. rewrite S_P in H.
+apply <- IH in H. apply -> lt_n_m_P in H. le_elim H.
+assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn.
+Qed.
+
+Theorem lt_Pn_m : forall n m, n < m -> P n < m.
+Proof.
+intros; rewrite lt_P; now le_intro1.
+Qed.
+
+Theorem le_Pn_m : forall n m, n <= m -> P n <= m.
+Proof.
+intros n m H; rewrite <- lt_P in H; now le_intro1.
+Qed.
+
+Theorem lt_n_m_S : forall n m, n < m <-> S n <= m.
+Proof.
+intros n m; rewrite_P_S n; rewrite S_P; apply lt_P.
+Qed.
+
+Theorem lt_Sn_m : forall n m, S n < m -> n < m.
+Proof.
+intros n m H; rewrite_P_S n; now apply lt_Pn_m.
+Qed.
+
+Theorem le_Sn_m : forall n m, S n <= m -> n <= m.
+Proof.
+intros n m H; rewrite <- lt_n_m_S in H; now le_intro1.
+Qed.
+
+Theorem lt_n_Pm : forall n m, n < P m -> n < m.
+Proof.
+intros n m H; rewrite_S_P m; now apply lt_n_Sm.
+Qed.
+
+Theorem le_n_Pm : forall n m, n <= P m -> n <= m.
+Proof.
+intros n m H; rewrite <- lt_n_m_P in H; now le_intro1.
+Qed.
+
+Theorem lt_respects_S : forall n m, n < m <-> S n < S m.
+Proof.
+intros n m. rewrite lt_n_m_S. symmetry. apply lt_S.
+Qed.
+
+Theorem le_respects_S : forall n m, n <= m <-> S n <= S m.
+Proof.
+intros n m. do 2 rewrite le_lt.
+firstorder using lt_respects_S S_wd S_inj.
+Qed.
+
+Theorem lt_respects_P : forall n m, n < m <-> P n < P m.
+Proof.
+intros n m. rewrite lt_n_m_P. symmetry; apply lt_P.
+Qed.
+
+Theorem le_respects_P : forall n m, n <= m <-> P n <= P m.
+Proof.
+intros n m. do 2 rewrite le_lt.
+firstorder using lt_respects_P P_wd P_inj.
+Qed.
+
+Theorem lt_S_P : forall n m, S n < m <-> n < P m.
+Proof.
+intros n m; rewrite_P_S n at 2; apply lt_respects_P.
+Qed.
+
+Theorem le_S_P : forall n m, S n <= m <-> n <= P m.
+Proof.
+intros n m; rewrite_P_S n at 2; apply le_respects_P.
+Qed.
+
+Theorem lt_P_S : forall n m, P n < m <-> n < S m.
+Proof.
+intros n m; rewrite_S_P n at 2; apply lt_respects_S.
+Qed.
+
+Theorem le_P_S : forall n m, P n <= m <-> n <= S m.
+Proof.
+intros n m; rewrite_S_P n at 2; apply le_respects_S.
+Qed.
+
+Theorem lt_neq : forall n m, n < m -> n # m.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
+Proof.
+intros n m; induct_n n m.
+intros p H _; false_hyp H lt_irr.
+intros n IH p H1 H2. apply lt_Sn_m in H1. pose proof (IH p H1 H2) as H3.
+rewrite lt_n_m_S in H3; le_elim H3.
+assumption. rewrite <- H3 in H2. rewrite lt_S in H2; le_elim H2.
+elimtype False; apply lt_irr with (n := n); now apply IH.
+rewrite H2 in H1; false_hyp H1 lt_irr.
+intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; le_elim H1.
+now apply IH. now rewrite H1.
+Qed.
+
+Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+le_elim H2. le_intro1; now apply lt_trans with (m := m).
+le_intro1; now rewrite <- H2. now rewrite H1.
+Qed.
+
+Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+now apply lt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+now apply lt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem lt_asymm : forall n m, n < m -> ~ m < n.
+Proof.
+intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+Qed.
+
+Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m.
+Proof.
+intros n m H1 H2; le_elim H1; le_elim H2.
+elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+now symmetry. assumption. assumption.
+Qed.
+
+Theorem not_lt_Sn_n : forall n, ~ S n < n.
+Proof.
+intros n H; apply (lt_asymm n (S n)). apply lt_n_Sn. assumption.
+Qed.
+
+Theorem not_le_Sn_n : forall n, ~ S n <= n.
+Proof.
+intros n H; le_elim H. false_hyp H not_lt_Sn_n.
+pose proof (lt_n_Sn n) as H1. rewrite H in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem lt_gt : forall n m, n < m -> m < n -> False.
+Proof.
+intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+Qed.
+
+Theorem lt_total : forall n m,  n < m \/ n == m \/ m < n.
+Proof.
+intros n m; induct_n n m.
+right; now left.
+intros n IH; destruct IH as [H | [H | H]].
+rewrite lt_n_m_S in H. rewrite le_lt in H; tauto.
+right; right; rewrite H; apply lt_n_Sn.
+right; right; now apply lt_n_Sm.
+intros n IH; destruct IH as [H | [H | H]].
+left; now apply lt_Pn_m.
+left; rewrite H; apply lt_Pn_n.
+rewrite lt_n_m_P in H. rewrite le_lt in H.
+setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto.
+split; intro; now symmetry.
+Qed.
+
+Theorem le_gt : forall n m, n <= m <-> ~ m < n.
+Proof.
+intros n m. rewrite -> le_lt.
+pose proof (lt_total n m). pose proof (lt_gt n m).
+assert (n == m -> ~ m < n); [intro A; rewrite A; apply lt_irr |].
+tauto.
+Qed.
+
+Theorem lt_ge : forall n m, n < m <-> ~ m <= n.
+Proof.
+intros n m. rewrite -> le_lt.
+pose proof (lt_total m n). pose proof (lt_gt n m).
+assert (n < m -> m # n); [intros A B; rewrite B in A; false_hyp A lt_irr |].
+tauto.
+Qed.
+
+Theorem lt_discrete : forall n m, n < m -> m < S n -> False.
+Proof.
+intros n m H1 H2; apply -> lt_S in H2; apply -> lt_ge in H1; false_hyp H2 H1.
+Qed.
+
+(* Decidability of order can be proved either from totality or from the fact
+that < and <= are boolean functions *)
+
+(** A corollary of having an order is that Z is infinite in both
+directions *)
+
+Theorem neq_Sn_n : forall n, S n # n.
+Proof.
+intros n H. pose proof (lt_n_Sn n) as H1. rewrite H in H1. false_hyp H1 lt_irr.
+Qed.
+
+Theorem neq_Pn_n : forall n, P n # n.
+Proof.
+intros n H. apply S_wd in H. rewrite S_P in H. now apply neq_Sn_n with (n := n).
+Qed.
+
+Lemma lt_n_Skn :
+  forall (n : Z) (k : nat), n < iter_nat (Datatypes.S k) Z S n.
+Proof.
+intro n; induction k as [| k IH]; simpl in *.
+apply lt_n_Sn. now apply lt_n_Sm.
+Qed.
+
+Lemma lt_Pkn_n :
+  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n < n.
+Proof.
+intro n; induction k as [| k IH]; simpl in *.
+apply lt_Pn_n. now apply lt_Pn_m.
+Qed.
+
+Theorem neq_n_Skn :
+  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z S n # n.
+Proof.
+intros n k H. pose proof (lt_n_Skn n k) as H1. rewrite H in H1.
+false_hyp H1 lt_irr.
+Qed.
+
+Theorem neq_Pkn_n :
+  forall (n : Z) (k : nat), iter_nat (Datatypes.S k) Z P n # n.
+Proof.
+intros n k H. pose proof (lt_Pkn_n n k) as H1. rewrite H in H1.
+false_hyp H1 lt_irr.
+Qed.
+
+(** Stronger variant of induction with assumptions n >= 0 (n <= 0)
+in the induction step *)
+
+Section Induction.
+
+Variable Q : Z -> Prop.
+Hypothesis Q_wd : pred_wd E Q.
+
+Add Morphism Q with signature E ==> iff as Q_morph.
+Proof Q_wd.
+
+Section Center.
+
+Variable z : Z. (* Q z is the basis of induction *)
+
+Section RightInduction.
+
+Let Q' := fun n : Z => forall m, z <= m -> m < n -> Q m.
+
+Add Morphism Q' with signature E ==> iff as Q'_pos_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem right_induction :
+  Q z -> (forall n, z <= n -> Q n -> Q (S n)) -> forall n, z <= n -> Q n.
+Proof.
+intros Qz QS k k_ge_z.
+assert (H : forall n, Q' n). induct_n n z; unfold Q'.
+intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
+intros n IH m H2 H3.
+rewrite lt_S in H3; le_elim H3. now apply IH.
+le_elim H2. rewrite_S_P m.
+apply QS. now apply -> lt_n_m_P. apply IH. now apply -> lt_n_m_P.
+rewrite H3; apply lt_Pn_n. now rewrite <- H2.
+intros n IH m H2 H3. apply IH. assumption. now apply lt_n_Pm.
+pose proof (H (S k)) as H1; unfold Q' in H1. apply H1.
+apply k_ge_z. apply lt_n_Sn.
+Qed.
+
+End RightInduction.
+
+Section LeftInduction.
+
+Let Q' := fun n : Z => forall m, m <= z -> n < m -> Q m.
+
+Add Morphism Q' with signature E ==> iff as Q'_neg_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem left_induction :
+  Q z -> (forall n, n <= z -> Q n -> Q (P n)) -> forall n, n <= z -> Q n.
+Proof.
+intros Qz QP k k_le_z.
+assert (H : forall n, Q' n). induct_n n z; unfold Q'.
+intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
+intros n IH m H2 H3. apply IH. assumption. now apply lt_Sn_m.
+intros n IH m H2 H3.
+rewrite lt_P in H3; le_elim H3. now apply IH.
+le_elim H2. rewrite_P_S m.
+apply QP. now apply -> lt_n_m_S. apply IH. now apply -> lt_n_m_S.
+rewrite H3; apply lt_n_Sn. now rewrite H2.
+pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
+apply k_le_z. apply lt_Pn_n.
+Qed.
+
+End LeftInduction.
+
+Theorem induction_ord_n :
+  Q z ->
+  (forall n, z <= n -> Q n -> Q (S n)) ->
+  (forall n, n <= z -> Q n -> Q (P n)) ->
+    forall n, Q n.
+Proof.
+intros Qz QS QP n.
+destruct (lt_total n z) as [H | [H | H]].
+now apply left_induction; [| | le_intro1].
+now rewrite H.
+now apply right_induction; [| | le_intro1].
+Qed.
+
+End Center.
+
+Theorem induction_ord :
+  Q 0 ->
+  (forall n, 0 <= n -> Q n -> Q (S n)) ->
+  (forall n, n <= 0 -> Q n -> Q (P n)) ->
+    forall n, Q n.
+Proof (induction_ord_n 0).
+
+Theorem lt_ind : forall (n : Z),
+  Q (S n) ->
+  (forall m : Z, n < m -> Q m -> Q (S m)) ->
+   forall m : Z, n < m -> Q m.
+Proof.
+intros n H1 H2 m H3.
+apply right_induction with (S n). assumption.
+intros; apply H2; try assumption. now apply <- lt_n_m_S.
+now apply -> lt_n_m_S.
+Qed.
+
+Theorem le_ind : forall (n : Z),
+  Q n ->
+  (forall m : Z, n <= m -> Q m -> Q (S m)) ->
+   forall m : Z, n <= m -> Q m.
+Proof.
+intros n H1 H2 m H3.
+now apply right_induction with n.
+Qed.
+
+End Induction.
+
+Ltac induct_ord n :=
+  try intros until n;
+  pattern n; apply induction_ord; 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 | | |].
+
+End OrderProperties.
+
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
new file mode 100644
index 000000000..1b5aa73fb
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -0,0 +1,222 @@
+Require Import NumPrelude.
+Require Import ZDomain.
+Require Import ZAxioms.
+
+Module Type PlusSignature.
+Declare Module Export IntModule : IntSignature.
+
+Parameter Inline plus : Z -> Z -> Z.
+Parameter Inline minus : Z -> Z -> Z.
+Parameter Inline uminus : Z -> Z.
+
+Notation "x + y" := (plus x y).
+Notation "x - y" := (minus x y).
+Notation "- x" := (uminus x).
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Add Morphism uminus with signature E ==> E as uminus_wd.
+
+Axiom plus_0 : forall n, 0 + n == n.
+Axiom plus_S : forall n m, (S n) + m == S (n + m).
+
+Axiom minus_0 : forall n, n - 0 == n.
+Axiom minus_S : forall n m, n - (S m) == P (n - m).
+
+Axiom uminus_0 : - 0 == 0.
+Axiom uminus_S : forall n, - (S n) == P (- n).
+
+End PlusSignature.
+
+Module PlusProperties (Export PlusModule : PlusSignature).
+
+Module Export IntPropertiesModule := IntProperties IntModule.
+
+Theorem plus_P : forall n m, P n + m == P (n + m).
+Proof.
+intros n m. rewrite_S_P n at 2. rewrite plus_S. now rewrite P_S.
+Qed.
+
+Theorem minus_P : forall n m, n - (P m) == S (n - m).
+Proof.
+intros n m. rewrite_S_P m at 2. rewrite minus_S. now rewrite S_P.
+Qed.
+
+Theorem uminus_P : forall n, - (P n) == S (- n).
+Proof.
+intro n. rewrite_S_P n at 2. rewrite uminus_S. now rewrite S_P.
+Qed.
+
+Theorem plus_n_0 : forall n, n + 0 == n.
+Proof.
+induct n.
+now rewrite plus_0.
+intros n IH. rewrite plus_S. now rewrite IH.
+intros n IH. rewrite plus_P. now rewrite IH.
+Qed.
+
+Theorem plus_n_Sm : forall n m, n + S m == S (n + m).
+Proof.
+intros n m; induct n.
+now do 2 rewrite plus_0.
+intros n IH. do 2 rewrite plus_S. now rewrite IH.
+intros n IH. do 2 rewrite plus_P. rewrite IH. rewrite P_S; now rewrite S_P.
+Qed.
+
+Theorem plus_n_Pm : forall n m, n + P m == P (n + m).
+Proof.
+intros n m; rewrite_S_P m at 2. rewrite plus_n_Sm; now rewrite P_S.
+Qed.
+
+Theorem plus_opp_minus : forall n m, n + (- m) == n - m.
+Proof.
+induct m.
+rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0.
+intros m IH. rewrite uminus_S; rewrite minus_S. rewrite plus_n_Pm; now rewrite IH.
+intros m IH. rewrite uminus_P; rewrite minus_P. rewrite plus_n_Sm; now rewrite IH.
+Qed.
+
+Theorem minus_0_n : forall n, 0 - n == - n.
+Proof.
+intro n; rewrite <- plus_opp_minus; now rewrite plus_0.
+Qed.
+
+Theorem minus_Sn_m : forall n m, S n - m == S (n - m).
+Proof.
+intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_S.
+Qed.
+
+Theorem minus_Pn_m : forall n m, P n - m == P (n - m).
+Proof.
+intros n m. rewrite_S_P n at 2; rewrite minus_Sn_m; now rewrite P_S.
+Qed.
+
+Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
+Proof.
+intros n m p; induct n.
+now do 2 rewrite plus_0.
+intros n IH. do 3 rewrite plus_S. now rewrite IH.
+intros n IH. do 3 rewrite plus_P. now rewrite IH.
+Qed.
+
+Theorem plus_comm : forall n m, n + m == m + n.
+Proof.
+intros n m; induct n.
+rewrite plus_0; now rewrite plus_n_0.
+intros n IH; rewrite plus_S; rewrite plus_n_Sm; now rewrite IH.
+intros n IH; rewrite plus_P; rewrite plus_n_Pm; now rewrite IH.
+Qed.
+
+Theorem minus_diag : forall n, n - n == 0.
+Proof.
+induct n.
+now rewrite minus_0.
+intros n IH. rewrite minus_S; rewrite minus_Sn_m; rewrite P_S; now rewrite IH.
+intros n IH. rewrite minus_P; rewrite minus_Pn_m; rewrite S_P; now rewrite IH.
+Qed.
+
+Theorem plus_opp_r : forall n, n + (- n) == 0.
+Proof.
+intro n; rewrite plus_opp_minus; now rewrite minus_diag.
+Qed.
+
+Theorem plus_opp_l : forall n, - n + n == 0.
+Proof.
+intro n; rewrite plus_comm; apply plus_opp_r.
+Qed.
+
+Theorem minus_swap : forall n m, - m + n == n - m.
+Proof.
+intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm.
+Qed.
+
+Theorem plus_minus_inverse : forall n m, n + (m - n) == m.
+Proof.
+intros n m; rewrite <- minus_swap. rewrite plus_assoc;
+rewrite plus_opp_r; now rewrite plus_0.
+Qed.
+
+Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p.
+Proof.
+intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc.
+Qed.
+
+Theorem double_opp : forall n, - (- n) == n.
+Proof.
+induct n.
+now do 2 rewrite uminus_0.
+intros n IH. rewrite uminus_S; rewrite uminus_P; now rewrite IH.
+intros n IH. rewrite uminus_P; rewrite uminus_S; now rewrite IH.
+Qed.
+
+Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m).
+Proof.
+intros n m; induct n.
+rewrite uminus_0; now do 2 rewrite plus_0.
+intros n IH. rewrite plus_S; do 2 rewrite uminus_S. rewrite IH. now rewrite plus_P.
+intros n IH. rewrite plus_P; do 2 rewrite uminus_P. rewrite IH. now rewrite plus_S.
+Qed.
+
+Theorem opp_minus_distr : forall n m, - (n - m) == - n + m.
+Proof.
+intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr.
+now rewrite double_opp.
+Qed.
+
+Theorem opp_inj : forall n m, - n == - m -> n == m.
+Proof.
+intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H.
+Qed.
+
+Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p.
+Proof.
+intros n m p; rewrite <- plus_opp_minus. rewrite opp_plus_distr. rewrite plus_assoc.
+now do 2 rewrite plus_opp_minus.
+Qed.
+
+Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p.
+Proof.
+intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc.
+now rewrite plus_opp_minus.
+Qed.
+
+Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m.
+Proof.
+intros n m p. rewrite <- plus_minus_distr.
+rewrite <- (plus_opp_minus n p). rewrite <- plus_assoc. now rewrite minus_swap.
+Qed.
+
+Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p.
+Proof.
+intros n m p H.
+assert (H1 : - n + n + m == -n + n + p).
+do 2 rewrite <- plus_assoc; now rewrite H.
+rewrite plus_opp_l in H1; now do 2 rewrite plus_0 in H1.
+Qed.
+
+Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p.
+Proof.
+intros n m p H.
+rewrite plus_comm in H. set (k := m + n) in H. rewrite plus_comm in H.
+unfold k in H; clear k. now apply plus_cancel_l with m.
+Qed.
+
+Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m.
+Proof.
+intros n m p H.
+assert (H1 : - m + m + p == - m + n).
+rewrite <- plus_assoc; now rewrite H.
+rewrite plus_opp_l in H1. rewrite plus_0 in H1. now rewrite minus_swap in H1.
+Qed.
+
+Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p.
+Proof.
+intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H.
+Qed.
+
+Lemma minus_eq : forall n m, n - m == 0 -> n == m.
+Proof.
+intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
+Qed.
+
+End PlusProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
new file mode 100644
index 000000000..abaaa664f
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -0,0 +1,160 @@
+Require Import ZOrder.
+Require Import ZPlus.
+(* Warning: Trying to mask the absolute name "Plus"!!! *)
+
+Module PlusOrderProperties (Export PlusModule : PlusSignature)
+                           (Export OrderModule : OrderSignature with
+                             Module IntModule := PlusModule.IntModule).
+
+Module Export PlusPropertiesModule := PlusProperties PlusModule.
+Module Export OrderPropertiesModule := OrderProperties OrderModule.
+
+Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
+Proof.
+intros n m p; induct p.
+now do 2 rewrite plus_0.
+intros p IH. do 2 rewrite plus_S. now rewrite <- lt_respects_S.
+intros p IH. do 2 rewrite plus_P. now rewrite <- lt_respects_P.
+Qed.
+
+Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p.
+Proof.
+intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
+apply plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; do 2 rewrite <- lt_S. rewrite <- plus_n_Sm;
+apply plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
+apply plus_le_compat_l.
+Qed.
+
+Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. apply lt_trans with (m := m + p).
+now apply -> plus_lt_compat_r. now apply -> plus_lt_compat_l.
+Qed.
+
+Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat.
+rewrite H2. now apply -> plus_lt_compat_r.
+Qed.
+
+Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat.
+rewrite H1. now apply -> plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat.
+rewrite H1. now apply -> plus_le_compat_l.
+Qed.
+
+Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof.
+intros; rewrite <- (plus_0 0); now apply plus_le_compat.
+Qed.
+
+Lemma lt_opp_forward : forall n m, n < m -> - m < - n.
+Proof.
+induct n.
+induct_ord m.
+intro H; false_hyp H lt_irr.
+intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *.
+le_elim H1. apply IH in H1. now apply lt_Pn_m.
+rewrite <- H1; rewrite uminus_0; apply lt_Pn_n.
+intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1.
+intros n IH m H. rewrite uminus_S.
+apply -> lt_S_P in H. apply IH in H. rewrite uminus_P in H. now apply -> lt_S_P.
+intros n IH m H. rewrite uminus_P.
+apply -> lt_P_S in H. apply IH in H. rewrite uminus_S in H. now apply -> lt_P_S.
+Qed.
+
+Theorem lt_opp : forall n m, n < m <-> - m < - n.
+Proof.
+intros n m; split.
+apply lt_opp_forward.
+intro; rewrite <- (double_opp n); rewrite <- (double_opp m);
+now apply lt_opp_forward.
+Qed.
+
+Theorem le_opp : forall n m, n <= m <-> - m <= - n.
+Proof.
+intros n m; do 2 rewrite -> le_lt; rewrite <- lt_opp.
+assert (n == m <-> - m == - n).
+split; intro; [now apply uminus_wd | now apply opp_inj].
+tauto.
+Qed.
+
+Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply lt_opp. now rewrite uminus_0.
+Qed.
+
+Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply le_opp. now rewrite uminus_0.
+Qed.
+
+Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply lt_opp. now rewrite uminus_0.
+Qed.
+
+Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply le_opp. now rewrite uminus_0.
+Qed.
+
+Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l.
+apply lt_opp.
+Qed.
+
+Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l.
+apply le_opp.
+Qed.
+
+Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r.
+Qed.
+
+Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r.
+Qed.
+
+Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p.
+Proof.
+intros n m p. rewrite (minus_lt_incr_l (n + p) m p).
+rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p.
+Proof.
+intros n m p. rewrite (minus_le_nondecr_l (n + p) m p).
+rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+End PlusOrderProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
new file mode 100644
index 000000000..3f9c7c4ce
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -0,0 +1,135 @@
+Require Import NumPrelude.
+Require Import ZDomain.
+Require Import ZAxioms.
+Require Import ZPlus.
+
+Module Type TimesSignature.
+Declare Module Export PlusModule : PlusSignature.
+
+Parameter Inline times : Z -> Z -> Z.
+
+Notation "x * y" := (times x y).
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+
+Axiom times_0 : forall n, n * 0 == 0.
+Axiom times_S : forall n m, n * (S m) == n * m + n.
+
+(* Here recursion is done on the second argument to conform to the
+usual definition of ordinal multiplication in set theory, which is not
+commutative. It seems, however, that this definition in set theory is
+unfortunate for two reasons. First, multiplication of two ordinals A
+and B can be defined as (an order type of) the cartesian product B x A
+(not A x B) ordered lexicographically. For example, omega * 2 =
+2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...},
+while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) <
+(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in
+French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not
+2 + 2 + 2. So it would possibly be more reasonable to define multiplication
+(here as well as in set theory) by recursion on the first argument. *)
+
+End TimesSignature.
+
+Module TimesProperties (Export TimesModule : TimesSignature).
+
+Module Export PlusPropertiesModule := PlusProperties PlusModule.
+
+Theorem times_P : forall n m, n * (P m) == n * m - n.
+Proof.
+intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr.
+rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+Theorem times_0_n : forall n, 0 * n == 0.
+Proof.
+induct n.
+now rewrite times_0.
+intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0.
+intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0.
+Qed.
+
+Theorem times_Sn_m : forall n m, (S n) * m == n * m + m.
+Proof.
+induct m.
+do 2 rewrite times_0. now rewrite plus_0.
+intros m IH. do 2 rewrite times_S. rewrite IH.
+do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity.
+do 2 rewrite plus_n_Sm; now rewrite plus_comm.
+intros m IH. do 2 rewrite times_P. rewrite IH.
+rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr.
+apply plus_wd. reflexivity.
+rewrite minus_S. now rewrite minus_Pn_m.
+Qed.
+
+Theorem times_Pn_m : forall n m, (P n) * m == n * m - m.
+Proof.
+intros n m. rewrite_S_P n at 2. rewrite times_Sn_m.
+rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0.
+Qed.
+
+Theorem times_comm : forall n m, n * m == m * n.
+Proof.
+intros n m; induct n.
+rewrite times_0_n; now rewrite times_0.
+intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH.
+intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH.
+Qed.
+
+Theorem times_opp_r : forall n m, n * (- m) == - (n * m).
+Proof.
+intros n m; induct m.
+rewrite uminus_0; rewrite times_0; now rewrite uminus_0.
+intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH.
+rewrite <- plus_opp_minus; now rewrite opp_plus_distr.
+intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH.
+now rewrite opp_minus_distr.
+Qed.
+
+Theorem times_opp_l : forall n m, (- n) * m == - (n * m).
+Proof.
+intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m);
+now rewrite times_opp_r.
+Qed.
+
+Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m.
+Proof.
+intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp.
+Qed.
+
+Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p.
+Proof.
+intros n m p; induct m.
+rewrite times_0; now do 2 rewrite plus_0.
+intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH.
+do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm].
+intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH.
+apply plus_minus_swap.
+Qed.
+
+Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p.
+Proof.
+intros n m p; rewrite (times_comm (n + m) p); rewrite times_plus_distr_r;
+rewrite (times_comm p n); now rewrite (times_comm p m).
+Qed.
+
+Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p.
+Proof.
+intros n m p.
+do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r.
+Qed.
+
+Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p.
+Proof.
+intros n m p.
+do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l.
+Qed.
+
+Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
+Proof.
+intros n m p; induct p.
+now do 3 rewrite times_0.
+intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH.
+intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH.
+Qed.
+
+End TimesProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
new file mode 100644
index 000000000..1f8b0a947
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -0,0 +1,92 @@
+Require Import ZPlus.
+Require Import ZTimes.
+Require Import ZOrder.
+(* Warning: Trying to mask the absolute name "Plus"!!! *)
+Require Import ZPlusOrder.
+
+Module TimesOrderProperties (Export TimesModule : TimesSignature)
+                            (Export OrderModule : OrderSignature with
+                              Module IntModule := TimesModule.PlusModule.IntModule).
+
+Module Export TimesPropertiesModule := TimesProperties TimesModule.
+Module Export PlusOrderPropertiesModule :=
+  PlusOrderProperties TimesModule.PlusModule OrderModule.
+
+Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p.
+Proof.
+intros n m p; induct_ord p.
+intros H _; false_hyp H lt_irr.
+intros p H IH H1 H2. do 2 rewrite times_S.
+apply -> lt_S in H1; le_elim H1.
+apply plus_lt_compat. now apply IH. assumption.
+rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0.
+intros p H IH H1 H2. apply lt_n_Pm in H1. apply -> le_gt in H.
+false_hyp H1 H.
+Qed.
+
+Theorem mult_lt_compat_l : forall n m p, 0 < p -> n < m -> p * n < p * m.
+Proof.
+intros n m p. rewrite (times_comm p n); rewrite (times_comm p m).
+apply mult_lt_compat_r.
+Qed.
+
+Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+le_intro1; now apply mult_lt_compat_r.
+rewrite H2. now le_intro2.
+Qed.
+
+Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m.
+Proof.
+intros n m p. rewrite (times_comm p n); rewrite (times_comm p m).
+apply mult_lt_le_compat_r.
+Qed.
+
+(* And so on *)
+
+Theorem mult_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
+Proof.
+intros n m; set (k := 0) in |-* at 3;
+setoid_replace k with (n * 0); unfold k; clear k.
+apply mult_lt_compat_l. now rewrite times_0.
+Qed.
+
+Theorem mult_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0.
+Proof.
+intros n m; set (k := 0) in |-* at 3;
+setoid_replace k with (n * 0); unfold k; clear k.
+apply mult_lt_compat_l. now rewrite times_0.
+Qed.
+(* The same proof script as for mult_pos_pos! *)
+
+Theorem mult_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0.
+Proof.
+intros n m H1 H2; rewrite times_comm; now apply mult_pos_neg.
+Qed.
+
+Theorem mult_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m.
+Proof.
+intros n m H1 H2. setoid_replace (n * m) with (- - (n * m));
+[| symmetry; apply double_opp].
+rewrite <- times_opp_l. rewrite <- times_opp_r.
+apply -> lt_opp_neg in H1. apply -> lt_opp_neg in H2.
+now apply mult_pos_pos.
+Qed.
+
+(** With order, Z is an integral domain *)
+Theorem mult_neq_0 : forall n m, n # 0 -> m # 0 -> n * m # 0.
+Proof.
+intros n m H1 H2.
+destruct (lt_total n 0) as [H3 | [H3 | H3]];
+destruct (lt_total m 0) as [H4 | [H4 | H4]].
+apply neq_symm. apply lt_neq. now apply mult_neg_neg.
+false_hyp H4 H2.
+apply lt_neq; now apply mult_neg_pos.
+false_hyp H3 H1. false_hyp H3 H1. false_hyp H3 H1.
+apply lt_neq; now apply mult_pos_neg.
+false_hyp H4 H2.
+apply neq_symm. apply lt_neq. now apply mult_pos_pos.
+Qed.
+
+End TimesOrderProperties.
diff --git a/theories/Numbers/Integer/NatPairs/CommRefl.v b/theories/Numbers/Integer/NatPairs/CommRefl.v
new file mode 100644
index 000000000..673a1fe50
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/CommRefl.v
@@ -0,0 +1,185 @@
+Require Import Arith.
+Require Import List.
+Require Import Setoid.
+
+Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
+
+Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin)
+  | x => node x fin
+  end.
+
+Fixpoint flatten (t:bin) : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten t2)
+  | x => x
+  end.
+
+Fixpoint nat_le_bool (n m:nat){struct m} : bool :=
+  match n, m with
+  | O, _ => true
+  | S _, O => false
+  | S n, S m => nat_le_bool n m
+  end.
+
+Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin :=
+  match t with
+  | leaf m => match nat_le_bool n m with
+              | true => node (leaf n)(leaf m)
+              | false => node (leaf m)(leaf n)
+              end
+  | node (leaf m) t' => match nat_le_bool n m with
+                        | true => node (leaf n) t
+                        | false => 
+                            node (leaf m)(insert_bin n t')
+                        end
+  | t => node (leaf n) t
+  end.
+
+Fixpoint sort_bin (t:bin) : bin :=
+  match t with
+  | node (leaf n) t' => insert_bin n (sort_bin t')
+  | t => t
+  end.
+
+Section commut_eq.
+Variable A : Set.
+Variable E : relation A.
+Variable f : A -> A -> A.
+
+Hypothesis E_equiv : equiv A E.
+Hypothesis comm : forall x y : A, f x y = f y x.
+Hypothesis assoc : forall x y z : A, f x (f y z) = f (f x y) z.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Add Relation A E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
+  match t with
+  | node t1 t2 => f (bin_A l def t1)(bin_A l def t2)
+  | leaf n => nth n l def
+  end.
+ Theorem flatten_aux_valid_A :
+ forall (l:list A)(def:A)(t t':bin),
+  f (bin_A l def t)(bin_A l def t') == bin_A l def (flatten_aux t t').
+Proof.
+ intros l def t; elim t; simpl; auto.
+ intros t1 IHt1 t2 IHt2 t'.  rewrite <- IHt1; rewrite <- IHt2.
+ symmetry; apply assoc.
+Qed.
+ Theorem flatten_valid_A :
+ forall (l:list A)(def:A)(t:bin),
+   bin_A l def t == bin_A l def (flatten t).
+Proof.
+ intros l def t; elim t; simpl; trivial.
+ intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2.
+ trivial.
+Qed.
+
+Theorem flatten_valid_A_2 :
+ forall (t t':bin)(l:list A)(def:A),
+   bin_A l def (flatten t) == bin_A l def (flatten t')->
+   bin_A l def t == bin_A l def t'. 
+Proof.
+ intros t t' l def Heq.
+ rewrite (flatten_valid_A l def t); rewrite (flatten_valid_A l def t').
+ trivial.
+Qed.
+
+Theorem insert_is_f : forall (l:list A)(def:A)(n:nat)(t:bin),
+   bin_A l def (insert_bin n t) == 
+   f (nth n l def) (bin_A l def t).
+Proof.
+ intros l def n t; elim t.
+ intros t1; case t1.
+ intros t1' t1'' IHt1 t2 IHt2.
+ simpl.
+ auto.
+ intros n0 IHt1 t2 IHt2.
+ simpl.
+ case (nat_le_bool n n0).
+ simpl.
+ auto.
+ simpl.
+ rewrite IHt2.
+ repeat rewrite assoc; rewrite (comm (nth n l def)); auto.
+ simpl.
+ intros n0; case (nat_le_bool n n0); auto.
+ rewrite comm; auto.
+Qed.
+
+Theorem sort_eq : forall (l:list A)(def:A)(t:bin),
+    bin_A l def (sort_bin t) == bin_A l def t.  
+Proof.
+ intros l def t; elim t.
+ intros t1 IHt1; case t1.
+ auto.
+ intros n t2 IHt2; simpl; rewrite insert_is_f.
+ rewrite IHt2; auto.
+ auto.
+Qed.
+
+
+Theorem sort_eq_2 :
+ forall (l:list A)(def:A)(t1 t2:bin),
+   bin_A l def (sort_bin t1) == bin_A l def (sort_bin t2)->
+   bin_A l def t1 == bin_A l def t2.  
+Proof.
+ intros l def t1 t2.
+ rewrite <- (sort_eq l def t1); rewrite <- (sort_eq l def t2).
+ trivial.
+Qed.
+
+End commut_eq.
+
+
+Ltac term_list f l v :=
+  match v with
+  | (f ?X1 ?X2) =>
+    let l1 := term_list f l X2 in term_list f l1 X1
+  | ?X1 => constr:(cons X1 l)
+  end.
+
+Ltac compute_rank l n v :=
+  match l with
+  | (cons ?X1 ?X2) =>
+    let tl := constr:X2 in
+    match constr:(X1 == v) with
+    | (?X1 == ?X1) => n
+    | _ => compute_rank tl (S n) v
+    end
+  end.
+
+Ltac model_aux l f v :=
+  match v with
+  | (f ?X1 ?X2) =>
+    let r1 := model_aux l f X1 with r2 := model_aux l f X2 in
+      constr:(node r1 r2)
+  | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n)
+  | _ => constr:(leaf 0)
+  end.
+
+Ltac comm_eq A f assoc_thm comm_thm :=
+  match goal with
+  | [ |- (?X1 == ?X2 :>A) ] =>
+    let l := term_list f (nil (A:=A)) X1 in
+    let term1 := model_aux l f X1 
+    with term2 := model_aux l f X2 in
+    (change (bin_A A f l X1 term1 == bin_A A f l X1 term2);
+      apply flatten_valid_A_2 with (1 := assoc_thm);
+      apply sort_eq_2 with (1 := comm_thm)(2 := assoc_thm); 
+      auto)
+  end.
+
+(*
+Theorem reflection_test4 : forall x y z:nat, x+(y+z) = (z+x)+y.
+Proof.
+ intros x y z. comm_eq nat plus plus_assoc plus_comm.
+Qed.
+*)
\ No newline at end of file
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
new file mode 100644
index 000000000..d2634970d
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -0,0 +1,45 @@
+Require Import NDomain.
+Require Import NAxioms.
+Require Import NPlus.
+Require Import NTimes.
+Require Import NLt.
+Require Import NPlusLt.
+Require Import NTimesLt.
+
+Require Import ZDomain.
+Require Import ZAxioms.
+Require Import ZPlus.
+Require Import ZTimes.
+Require Import ZOrder.
+Require Import ZPlusOrder.
+Require Import ZTimesOrder.
+
+Module NatPairsDomain (Export PlusModule : NPlus.PlusSignature) <:
+  ZDomain.DomainSignature.
+
+Module Export PlusPropertiesModule := NPlus.PlusProperties PlusModule.
+
+Definition Z : Set := (N * N)%type.
+Definition E (p1 p2 : Z) := (fst p1) + (snd p2) == (fst p2) + (snd p1).
+Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
+
+Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
+Proof.
+intros x y; unfold E, e; apply E_equiv_e.
+Qed.
+
+Theorem E_equiv : equiv Z E.
+Proof.
+split; [| split]; unfold reflexive, symmetric, transitive, E.
+now intro x.
+intros x y z H1 H2.
+comm_eq N 
+
+
+
+assert (H : ((fst x) + (snd y)) + ((fst y) + (snd z)) ==
+            ((fst y) + (snd x)) + ((fst z) + (snd y))); [now apply plus_wd |].
+assert (H : (fst y) + (snd y) + (fst x) + (snd z) ==
+            (fst y) + (snd y) + (snd x) + (fst z)).
+
+
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.*)
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
new file mode 100644
index 000000000..2fe547681
--- /dev/null
+++ b/theories/Numbers/NumPrelude.v
@@ -0,0 +1,324 @@
+Require Export Setoid.
+
+(*
+Contents:
+- Coercion from bool to Prop
+- An attempt to extend setoid rewrite to formulas with quantifiers
+- Extentional properties of predicates, relations and functions
+  (well-definedness and equality)
+- Relations on cartesian product
+- Some boolean functions on nat
+- Miscellaneous
+*)
+
+(** Coercion from bool to Prop *)
+
+Definition eq_bool := (@eq bool).
+
+Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+Coercion eq_true : bool >-> Sortclass.
+
+Theorem neg_eq_true : forall x : bool, ~ x -> x = false.
+Proof.
+intros x H; destruct x; [elim (H is_eq_true) | reflexivity].
+Qed.
+
+(** An attempt to extend setoid rewrite to formulas with quantifiers *)
+
+(* The following algorithm was explained to me by Bruno Barras.
+
+In the future, we need to prove that some predicates are
+well-defined w.r.t. a setoid relation, i.e., we need to prove theorems
+of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it
+makes sense to do induction only on predicates that satisfy this
+property. Ideally, such goal should be proved by saying "intros x y H;
+rewrite H; reflexivity".
+
+Now, such predicates P may contain quantifiers besides setoid
+morphisms. However, the tactic "rewrite" (which in this case stands
+for "setoid_rewrite") currently cannot handle universal quantifiers as
+well as lambda abstractions, which are part of the existential
+quantifier notation (recall that "exists x, P" stands for "ex (fun x
+=> p)").
+
+Therefore, to prove that P x <-> P y, we proceed as follows. Suppose
+that P x is C[forall z, Q[x,z]] where C is a context, i.e., a term
+with a hole. We assume that the hole of C does not occur inside
+another quantifier, i.e., that forall z, Q[x,z] is a top-level
+quantifier in P. The notation Q[x,z] means that the term Q contains
+free occurrences of variables x and z. We prove that forall z, Q[x,z]
+<-> forall z, Q[y,z]. To do this, we show that forall z, Q[x,z] <->
+Q[y,z]. After performing "intro z", this goal is handled recursively,
+until no more quantifiers are left in Q.
+
+After we obtain the goal
+
+H : x == y
+H1 : forall z, Q[x,z] <-> forall z, Q[y,z]
+=================================
+C[forall z, Q[x,z]] <-> C[forall z, Q[y,z]]
+
+we say "rewrite H1". Repeating this for other quantifier subformulas
+in P, we make them all identical in P x and P y. After that, saying
+"rewrite H" solves the goal.
+
+To implement this algorithm, we need the following theorems:
+
+Theorem forall_morphism :
+  forall (A : Set) (P Q : A -> Prop),
+    (forall x : A, P x <-> Q x) -> ((forall x : A, P x) <-> (forall x : A, Q x)).
+
+Theorem exists_morphism :
+  forall (A : Set) (P Q : A -> Prop),
+    (forall x : A, P x <-> Q x) -> (ex P <-> ex Q)
+
+Below, we obtain them by registering the universal and existential
+quantifiers as setoid morphisms, though they can be proved without any
+reference to setoids. Ideally, registering quantifiers as morphisms
+should take care of setoid rewriting in the presence of quantifiers,
+but as described above, this is currently not so, and we have to
+handle quantifiers manually.
+
+The job of deriving P x <-> P y from x == y is done by the tactic
+qmorphism x y below. *)
+
+Section Quantifiers.
+
+Variable A : Set.
+
+Definition predicate := A -> Prop.
+
+Definition equiv_predicate : relation predicate :=
+  fun (P1 P2 : predicate) => forall x : A, P1 x <-> P2 x.
+
+Theorem equiv_predicate_refl : reflexive predicate equiv_predicate.
+Proof.
+unfold reflexive, equiv_predicate. reflexivity.
+Qed.
+
+Theorem equiv_predicate_symm : symmetric predicate equiv_predicate.
+Proof.
+firstorder.
+Qed.
+
+Theorem equiv_predicate_trans : transitive predicate equiv_predicate.
+Proof.
+firstorder.
+Qed.
+
+Add Relation predicate equiv_predicate
+  reflexivity proved by equiv_predicate_refl
+  symmetry proved by equiv_predicate_symm
+  transitivity proved by equiv_predicate_trans
+as equiv_predicate_rel.
+
+Add Morphism (@ex A)
+  with signature equiv_predicate ==> iff
+  as exists_morphism.
+Proof.
+firstorder.
+Qed.
+
+Add Morphism (fun P : predicate => forall x : A, P x)
+  with signature equiv_predicate ==> iff
+  as forall_morphism.
+Proof.
+firstorder.
+Qed.
+
+End Quantifiers.
+
+(* replace x by y in t *)
+Ltac repl x y t :=
+match t with
+| context C [x] => let t' := (context C [y]) in repl x y t'
+| _ => t
+end.
+
+Ltac qmorphism x y :=
+lazymatch goal with
+| |- ?P <-> ?P => reflexivity
+| |- context [ex ?P] =>
+  match P with
+  | context [x] =>
+    let P' := repl x y P in
+      setoid_replace (ex P) with (ex P') using relation iff;
+      [qmorphism x y |
+       apply exists_morphism; unfold equiv_predicate; intros; qmorphism x y]
+  end
+| |- context [forall z, @?P z] =>
+  match P with
+  | context [x] =>
+    let P' := repl x y P in
+      setoid_replace (forall z, P z) with (forall z, P' z) using relation iff;
+      [qmorphism x y |
+       apply forall_morphism; unfold equiv_predicate; intros; qmorphism x y]
+  end
+| _ => setoid_replace x with y; [reflexivity | assumption]
+end.
+
+(** Extentional properties of predicates, relations and functions *)
+
+Section ExtensionalProperties.
+
+Variables A B C : Set.
+Variable EA : relation A.
+Variable EB : relation B.
+Variable EC : relation C.
+
+(* "wd" stands for "well-defined" *)
+
+Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y).
+
+Definition fun2_wd (f : A -> B -> C) :=
+  forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y').
+
+Definition pred_wd (P : predicate A) :=
+  forall x y, EA x y -> (P x <-> P y).
+
+Definition rel_wd (R : relation A) :=
+  forall x x', EA x x' -> forall y y', EA y y' -> (R x y <-> R x' y').
+
+Definition eq_fun : relation (A -> B) :=
+  fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x').
+
+(* Note that reflexivity of eq_fun means that every function
+is well-defined w.r.t. EA and EB, i.e.,
+forall x x' : A, EA x x' -> EB (f x) (f x') *)
+
+Definition eq_fun2 (f f' : A -> B -> C) :=
+  forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f' x' y').
+
+End ExtensionalProperties.
+
+Implicit Arguments fun_wd [A B].
+Implicit Arguments fun2_wd [A B C].
+Implicit Arguments eq_fun [A B].
+Implicit Arguments eq_fun2 [A B C].
+Implicit Arguments pred_wd [A].
+Implicit Arguments rel_wd [A].
+
+(** Relations on cartesian product. Used in MiscFunct for defining
+functions whose domain is a product of sets by primitive recursion *)
+
+Section RelationOnProduct.
+
+Variables A B : Set.
+Variable EA : relation A.
+Variable EB : relation B.
+
+Hypothesis EA_equiv : equiv A EA.
+Hypothesis EB_equiv : equiv B EB.
+
+Definition prod_rel : relation (A * B) :=
+  fun p1 p2 => EA (fst p1) (fst p2) /\ EB (snd p1) (snd p2).
+
+Lemma prod_rel_refl : reflexive (A * B) prod_rel.
+Proof.
+unfold reflexive, prod_rel.
+destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
+Qed.
+
+Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Proof.
+unfold symmetric, prod_rel.
+destruct x; destruct y;
+split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto.
+Qed.
+
+Lemma prod_rel_trans : transitive (A * B) prod_rel.
+Proof.
+unfold transitive, prod_rel.
+destruct x; destruct y; destruct z; simpl.
+intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) |
+apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto.
+Qed.
+
+Theorem prod_rel_equiv : equiv (A * B) prod_rel.
+Proof.
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+Qed.
+
+End RelationOnProduct.
+
+Implicit Arguments prod_rel [A B].
+Implicit Arguments prod_rel_equiv [A B].
+
+(** Some boolean functions on nat. Their analogs are available in the
+standard library; however, we provide simpler definitions. Used in
+defining  implementations of natural numbers. *)
+
+Fixpoint eq_nat_bool (x y : nat) {struct x} : bool :=
+match x, y with
+| 0, 0 => true
+| S x', S y' => eq_nat_bool x' y'
+| _, _ => false
+end.
+
+Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y -> x = y.
+Proof.
+induction x; destruct y; simpl; intro H; try (reflexivity || inversion H).
+apply IHx in H; now rewrite H.
+Qed.
+
+Theorem eq_nat_bool_refl : forall x, eq_nat_bool x x.
+Proof.
+induction x; now simpl.
+Qed.
+
+(* The boolean less function can be defined as
+fun n m => proj1_sig (nat_lt_ge_bool n m)
+using the standard library.
+However, this definitionseems too complex. First, there are many
+functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
+using bool_of_sumbool and
+lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
+where the latter function is defined using sumbool_not and
+le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
+Second, this definition is not the most efficient, especially since
+le_lt_dec is proved using tactics, not by giving the explicit proof term. *)
+
+Fixpoint lt_bool (n m : nat) {struct n} : bool :=
+match n, m with
+| 0, S _ => true
+| S n', S m' => lt_bool n' m'
+| _, 0 => false
+end.
+
+(* The following properties are used both in Peano.v and in MPeano.v *)
+
+Theorem lt_bool_0 : forall x, ~ (lt_bool x 0).
+Proof.
+destruct x as [|x]; simpl; now intro.
+Qed.
+
+Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y.
+Proof.
+induction x as [| x IH]; destruct y as [| y]; simpl.
+split; [now right | now intro].
+split; [now left | now intro].
+split; [intro H; false_hyp H lt_bool_0 |
+intro H; destruct H as [H | H]; now auto].
+assert (H : x = y <-> S x = S y); [split; auto|].
+rewrite <- H; apply IH.
+Qed.
+
+(** Miscellaneous *)
+
+Definition less_than (x : comparison) : bool :=
+match x with Lt => true | _ => false end.
+
+Definition LE_Set : forall A : Set, relation A := (@eq).
+
+Lemma eq_equiv : forall A : Set, equiv A (LE_Set A).
+Proof.
+intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive.
+repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
+(* It is interesting how the tactic split proves reflexivity *)
+Qed.
+
+Add Relation (fun A : Set => A) LE_Set
+ reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
+ symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
+ transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
+as EA_rel.