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

9 files changed, 1448 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
new file mode 100644
index 0000000000..4f0eab8e35
--- /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 0000000000..00eab8842f
--- /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 0000000000..b1983d6f7f
--- /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 0000000000..1b5aa73fb2
--- /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 0000000000..abaaa664f7
--- /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 0000000000..3f9c7c4ce6
--- /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 0000000000..1f8b0a9478
--- /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 0000000000..673a1fe50d
--- /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 0000000000..d2634970db
--- /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)).
+
+