Update on theories/Numbers. Natural numbers are mostly complete,

need to make NZOrdAxiomsSig a subtype of NAxiomsSig.


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

47 files changed, 3504 insertions, 895 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
new file mode 100644
index 000000000..4019b4774
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -0,0 +1,160 @@
+Require Export NumPrelude.
+Require Export NZAxioms.
+
+Set Implicit Arguments.
+
+Module Type ZAxiomsSig.
+
+Parameter Inline Z : Set.
+Parameter Inline ZE : Z -> Z -> Prop.
+Parameter Inline Z0 : Z.
+Parameter Inline Zsucc : Z -> Z.
+Parameter Inline Zpred : Z -> Z.
+Parameter Inline Zplus : Z -> Z -> Z.
+Parameter Inline Zminus : Z -> Z -> Z.
+Parameter Inline Ztimes : Z -> Z -> Z.
+Parameter Inline Zlt : Z -> Z -> Prop.
+Parameter Inline Zle : Z -> Z -> Prop.
+
+Delimit Scope IntScope with Int.
+Open Local Scope IntScope.
+Notation "x == y" := (ZE x y) (at level 70, no associativity) : IntScope.
+Notation "x ~= y" := (~ ZE x y) (at level 70, no associativity) : IntScope.
+Notation "0" := Z0 : IntScope.
+Notation "'S'" := Zsucc : IntScope.
+Notation "'P'" := Zpred : IntScope.
+Notation "1" := (S 0) : IntScope.
+Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x < y" := (Zlt x y) : IntScope.
+Notation "x <= y" := (Zle x y) : IntScope.
+Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+
+Axiom ZE_equiv : equiv Z ZE.
+
+Add Relation Z ZE
+ reflexivity proved by (proj1 ZE_equiv)
+ symmetry proved by (proj2 (proj2 ZE_equiv))
+ transitivity proved by (proj1 (proj2 ZE_equiv))
+as ZE_rel.
+
+Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
+Add Morphism Zpred with signature ZE ==> ZE as Zpred_wd.
+Add Morphism Zplus with signature ZE ==> ZE ==> ZE as Zplus_wd.
+Add Morphism Zminus with signature ZE ==> ZE ==> ZE as Zminus_wd.
+Add Morphism Ztimes with signature ZE ==> ZE ==> ZE as Ztimes_wd.
+Add Morphism Zlt with signature ZE ==> ZE ==> iff as Zlt_wd.
+Add Morphism Zle with signature ZE ==> ZE ==> iff as Zle_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 (Import IntModule : IntSignature).
+Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule.
+Open Local Scope IntScope.
+
+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.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index e0b753d4e..e0b753d4e 100644
--- a/theories/Numbers/Integer/Axioms/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
diff --git a/theories/Numbers/Integer/Axioms/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v
index 9a7aaa099..9a7aaa099 100644
--- a/theories/Numbers/Integer/Axioms/ZDec.v
+++ b/theories/Numbers/Integer/Abstract/ZDec.v
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 028128cf7..028128cf7 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index cc834b442..cc834b442 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index 624f85f04..624f85f04 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 95f0fa8c6..95f0fa8c6 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
diff --git a/theories/Numbers/Integer/Axioms/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v
index ffcb2dea8..ffcb2dea8 100644
--- a/theories/Numbers/Integer/Axioms/ZPred.v
+++ b/theories/Numbers/Integer/Abstract/ZPred.v
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 38311aa2b..38311aa2b 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 055342bcc..055342bcc 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v
new file mode 100644
index 000000000..f5c19c611
--- /dev/null
+++ b/theories/Numbers/Integer/BigInts/EZBase.v
@@ -0,0 +1,167 @@
+Require Export ZBase.
+(*Require Import BigN.*)
+Require Import NMake.
+Require Import ZnZ.
+Require Import Basic_type.
+Require Import ZAux.
+Require Import Zeqmod.
+Require Import ZArith.
+
+Module EZBaseMod (Import EffIntsMod : W0Type) <: ZBaseSig.
+Open Local Scope Z_scope.
+
+Definition Z := EffIntsMod.w.
+
+Definition w_op := EffIntsMod.w_op.
+Definition w_spec := EffIntsMod.w_spec.
+Definition to_Z := w_op.(znz_to_Z).
+Definition of_Z := znz_of_Z w_op.
+Definition wB := base w_op.(znz_digits).
+
+Theorem Zpow_gt_1 : forall n m : BinInt.Z, 0 < n -> 1 < m -> 1 < m ^ n.
+Proof.
+intros n m H1 H2.
+replace 1 with (m ^ 0) by apply Zpower_exp_0.
+apply Zpower_lt_monotone; auto with zarith.
+Qed.
+
+Theorem wB_gt_1 : 1 < wB.
+Proof.
+unfold wB, base. apply Zpow_gt_1; unfold Zlt; auto with zarith.
+Qed.
+
+Theorem wB_gt_0 : 0 < wB.
+Proof.
+pose proof wB_gt_1; auto with zarith.
+Qed.
+
+Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).
+
+Theorem to_Z_spec : forall x : Z, 0 <= [|x|] < wB.
+Proof w_spec.(spec_to_Z).
+
+Definition ZE (n m : Z) := [|n|] = [|m|].
+
+Notation "x == y"  := (ZE x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope.
+Open Local Scope IntScope.
+
+Theorem ZE_equiv : equiv Z ZE.
+Proof.
+unfold equiv, reflexive, symmetric, transitive, ZE; repeat split; intros; auto.
+now transitivity [|y|].
+Qed.
+
+Add Relation Z ZE
+ reflexivity proved by (proj1 ZE_equiv)
+ symmetry proved by (proj2 (proj2 ZE_equiv))
+ transitivity proved by (proj1 (proj2 ZE_equiv))
+as ZE_rel.
+
+Definition Z0 := w_op.(znz_0).
+Definition Zsucc := w_op.(znz_succ).
+
+Notation "0" := Z0 : IntScope.
+Notation "'S'" := Zsucc : IntScope.
+Notation "1" := (S 0) : IntScope.
+
+Theorem Zsucc_spec : forall n : Z, [|S n|] = ([|n|] + 1) mod wB.
+Proof w_spec.(spec_succ).
+
+Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
+Proof.
+unfold ZE; intros n m H. do 2 rewrite Zsucc_spec. now rewrite H.
+Qed.
+
+Theorem Zsucc_inj : forall x y : Z, S x == S y -> x == y.
+Proof.
+intros x y H; unfold ZE in *; do 2 rewrite Zsucc_spec in H.
+apply <- Zplus_eqmod_compat_r in H.
+do 2 rewrite Zmod_def_small in H; now try apply to_Z_spec.
+apply wB_gt_0.
+Qed.
+
+Lemma of_Z_0 : of_Z 0 == Z0.
+Proof.
+unfold ZE, to_Z, of_Z. rewrite znz_of_Z_correct.
+symmetry; apply w_spec.(spec_0).
+exact w_spec. split; [auto with zarith |apply wB_gt_0].
+Qed.
+
+Section Induction.
+
+Variable A : Z -> Prop.
+Hypothesis A_wd : predicate_wd ZE A.
+Hypothesis A0 : A 0.
+Hypothesis AS : forall n : Z, A n <-> A (S n). (* In fact, it's enought to have only -> *)
+
+Add Morphism A with signature ZE ==> iff as A_morph.
+Proof A_wd.
+
+Let B (n : BinInt.Z) := A (of_Z n).
+
+Lemma B0 : B 0.
+Proof.
+unfold B. now rewrite of_Z_0.
+Qed.
+
+Lemma BS : forall n : BinInt.Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
+Proof.
+intros n H1 H2 H3.
+unfold B in *. apply -> AS in H3.
+setoid_replace (of_Z (n + 1)) with (S (of_Z n)) using relation ZE. assumption.
+unfold ZE. rewrite Zsucc_spec.
+unfold to_Z, of_Z. rewrite znz_of_Z_correct. rewrite znz_of_Z_correct.
+symmetry; apply Zmod_def_small; auto with zarith.
+exact w_spec.
+unfold wB in *; auto with zarith.
+exact w_spec.
+unfold wB in *; auto with zarith.
+Qed.
+
+Lemma Zbounded_induction :
+  (forall Q : BinInt.Z -> Prop, forall b : BinInt.Z,
+    Q 0 ->
+    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
+      forall n, 0 <= n -> n < b -> Q n)%Z.
+Proof.
+intros Q b Q0 QS.
+set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).
+assert (H : forall n, 0 <= n -> Q' n).
+apply natlike_rec2; unfold Q'.
+destruct (Zle_or_lt b 0) as [H | H]. now right. left; now split.
+intros n H IH. destruct IH as [[IH1 IH2] | IH].
+destruct (Zle_or_lt (b - 1) n) as [H1 | H1].
+right; auto with zarith.
+left. split; [auto with zarith | now apply (QS n)].
+right; auto with zarith.
+unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
+assumption. apply Zle_not_lt in H3. false_hyp H2 H3.
+Qed.
+
+Lemma B_holds : forall n : BinInt.Z, 0 <= n < wB -> B n.
+Proof.
+intros n [H1 H2].
+apply Zbounded_induction with wB.
+apply B0. apply BS. assumption. assumption.
+Qed.
+
+Theorem Zinduction : forall n : Z, A n.
+Proof.
+intro n. setoid_replace n with (of_Z (to_Z n)) using relation ZE.
+apply B_holds. apply to_Z_spec.
+unfold ZE, to_Z, of_Z; rewrite znz_of_Z_correct.
+reflexivity.
+exact w_spec.
+apply to_Z_spec.
+Qed.
+
+End Induction.
+
+End EZBaseMod.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v
new file mode 100644
index 000000000..ca3286211
--- /dev/null
+++ b/theories/Numbers/Integer/BigInts/Zeqmod.v
@@ -0,0 +1,48 @@
+Require Import ZArith.
+Require Import ZAux.
+
+Open Local Scope Z_scope.
+Notation "x == y '[' 'mod' z ']'" := ((x mod z) = (y mod z))
+  (at level 70, no associativity) : Z_scope.
+
+Theorem Zeqmod_refl : forall p n : Z, n == n [mod p].
+Proof.
+reflexivity.
+Qed.
+
+Theorem Zeqmod_symm : forall p n m : Z, n == m [mod p] -> m == n [mod p].
+Proof.
+now symmetry.
+Qed.
+
+Theorem Zeqmod_trans :
+  forall p n m k : Z, n == m [mod p] -> m == k [mod p] -> n == k [mod p].
+Proof.
+intros p n m k H1 H2; now transitivity (m mod p).
+Qed.
+
+Theorem Zplus_eqmod_compat_l :
+  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> k + n == k + m [mod p]).
+intros p n m k H1.
+assert (LR : forall n' m' k' : Z, n' == m' [mod p] -> k' + n' == k' + m' [mod p]).
+intros n' m' k' H2.
+pattern ((k' + n') mod p); rewrite Zmod_plus; [| assumption].
+pattern ((k' + m') mod p); rewrite Zmod_plus; [| assumption].
+rewrite H2. apply Zeqmod_refl.
+split; [apply LR |].
+intro H2. apply (LR (k + n) (k + m) (-k)) in H2.
+do 2 rewrite Zplus_assoc in H2. rewrite Zplus_opp_l in H2.
+now do 2 rewrite Zplus_0_l in H2.
+Qed.
+
+Theorem Zplus_eqmod_compat_r :
+  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> n + k == m + k [mod p]).
+intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k);
+apply Zplus_eqmod_compat_l.
+Qed.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
new file mode 100644
index 000000000..217d08850
--- /dev/null
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -0,0 +1,204 @@
+Require Import ZTimesOrder.
+Require Import ZArith.
+
+Open Local Scope Z_scope.
+Module Export ZBinDomain <: ZDomainSignature.
+Delimit Scope IntScope with Int.
+(* Is this really necessary? Without it, applying ZDomainProperties
+functor to this module produces an error since the functor opens the
+scope. *)
+
+Definition Z := Z.
+Definition E := (@eq Z).
+Definition e := Zeq_bool.
+
+Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
+Proof.
+intros x y; unfold E, e, Zeq_bool; split; intro H.
+rewrite H; now rewrite Zcompare_refl.
+rewrite eq_true_unfold_pos in H.
+assert (H1 : (x ?= y) = Eq).
+case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
+[reflexivity | discriminate H | discriminate H].
+now apply Zcompare_Eq_eq.
+Qed.
+
+Theorem E_equiv : equiv Z E.
+Proof.
+apply eq_equiv with (A := Z). (* It does not work without "with (A := Z)" though it looks like it should *)
+Qed.
+
+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.
+
+End ZBinDomain.
+
+Module Export ZBinInt <: IntSignature.
+Module Export ZDomainModule := ZBinDomain.
+
+Definition O := 0.
+Definition S := Zsucc'.
+Definition P := Zpred'.
+
+Add Morphism S with signature E ==> E as S_wd.
+Proof.
+intros; unfold E; congruence.
+Qed.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+intros; unfold E; congruence.
+Qed.
+
+Theorem S_inj : forall x y : Z, S x = S y -> x = y.
+Proof.
+exact Zsucc'_inj.
+Qed.
+
+Theorem S_P : forall x : Z, S (P x) = x.
+Proof.
+exact Zsucc'_pred'.
+Qed.
+
+Theorem 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.
+Proof.
+intros; now apply Zind.
+Qed.
+
+End ZBinInt.
+
+Module Export ZBinPlus <: ZPlusSignature.
+Module Export IntModule := ZBinInt.
+
+Definition plus := Zplus.
+Definition minus := Zminus.
+Definition uminus := Zopp.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Add Morphism uminus with signature E ==> E as uminus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Theorem plus_0 : forall n, 0 + n = n.
+Proof.
+exact Zplus_0_l.
+Qed.
+
+Theorem plus_S : forall n m, (S n) + m = S (n + m).
+Proof.
+intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
+Qed.
+
+Theorem minus_0 : forall n, n - 0 = n.
+Proof.
+exact Zminus_0_r.
+Qed.
+
+Theorem minus_S : forall n m, n - (S m) = P (n - m).
+Proof.
+intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
+apply Zminus_succ_r.
+Qed.
+
+Theorem uminus_0 : - 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem uminus_S : forall n, - (S n) = P (- n).
+Admitted.
+
+End ZBinPlus.
+
+Module Export ZBinTimes <: ZTimesSignature.
+Module Export ZPlusModule := ZBinPlus.
+
+Definition times := Zmult.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem times_0 : forall n, n * 0 = 0.
+Proof.
+exact Zmult_0_r.
+Qed.
+
+Theorem times_S : forall n m, n * (S m) = n * m + n.
+Proof.
+intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r.
+Qed.
+
+End ZBinTimes.
+
+Module Export ZBinOrder <: ZOrderSignature.
+Module Export IntModule := ZBinInt.
+
+Definition lt := Zlt_bool.
+Definition le := Zle_bool.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
+Proof.
+intros; unfold lt, le, Zlt_bool, Zle_bool.
+case_eq (n ?= m); intro H.
+apply Zcompare_Eq_eq in H; rewrite H; now split; intro; [right |].
+now split; intro; [left |].
+split; intro H1. now idtac.
+destruct H1 as [H1 | H1].
+assumption. unfold E in H1; rewrite H1 in H. now rewrite Zcompare_refl in H.
+Qed.
+
+Theorem lt_irr : forall n, ~ (lt n n).
+Proof.
+intro n; rewrite eq_true_unfold_pos; intro H.
+assert (H1 : (Zlt n n)).
+change (if true then (Zlt n n) else (Zge n n)). rewrite <- H.
+unfold lt. apply Zlt_cases.
+false_hyp H1 Zlt_irrefl.
+Qed.
+
+Theorem lt_S : forall n m, lt n (S m) <-> le n m.
+Proof.
+intros; unfold lt, le, S; do 2 rewrite eq_true_unfold_pos.
+rewrite <- Zsucc_succ'; rewrite <- Zlt_is_lt_bool; rewrite <- Zle_is_le_bool.
+split; intro; [now apply Zlt_succ_le | now apply Zle_lt_succ].
+Qed.
+
+End ZBinOrder.
+
+Module Export ZTimesOrderPropertiesModule :=
+  ZTimesOrderProperties ZBinTimes ZBinOrder.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/Makefile b/theories/Numbers/NatInt/Makefile
new file mode 100644
index 000000000..e23d8dee2
--- /dev/null
+++ b/theories/Numbers/NatInt/Makefile
@@ -0,0 +1,4 @@
+.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
+
+.v.vo:
+	coqtop -boot -compile $*
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
new file mode 100644
index 000000000..fa0bd21a3
--- /dev/null
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -0,0 +1,72 @@
+Require Export NumPrelude.
+
+Module Type NZAxiomsSig.
+
+Parameter Inline NZ : Set.
+Parameter Inline NZE : NZ -> NZ -> Prop.
+Parameter Inline NZ0 : NZ.
+Parameter Inline NZsucc : NZ -> NZ.
+Parameter Inline NZpred : NZ -> NZ.
+Parameter Inline NZplus : NZ -> NZ -> NZ.
+Parameter Inline NZtimes : NZ -> NZ -> NZ.
+
+Axiom NZE_equiv : equiv NZ NZE.
+Add Relation NZ NZE
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
+
+Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+
+Delimit Scope NatIntScope with NatInt.
+Open Local Scope NatIntScope.
+Notation "x == y"  := (NZE x y) (at level 70) : NatIntScope.
+Notation "x ~= y" := (~ NZE x y) (at level 70) : NatIntScope.
+Notation "0" := NZ0 : NatIntScope.
+Notation "'S'" := NZsucc : NatIntScope.
+Notation "'P'" := NZpred : NatIntScope.
+Notation "1" := (S 0) : NatIntScope.
+Notation "x + y" := (NZplus x y) : NatIntScope.
+Notation "x * y" := (NZtimes x y) : NatIntScope.
+
+Axiom NZpred_succ : forall n : NZ, P (S n) == n.
+
+Axiom NZinduction :
+  forall A : NZ -> Prop, predicate_wd NZE A ->
+    A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
+
+Axiom NZplus_0_l : forall n : NZ, 0 + n == n.
+Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+
+Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0.
+Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+
+End NZAxiomsSig.
+
+Module Type NZOrdAxiomsSig.
+Declare Module Export NZAxiomsMod : NZAxiomsSig.
+Open Local Scope NatIntScope.
+
+Parameter Inline NZlt : NZ -> NZ -> Prop.
+Parameter Inline NZle : NZ -> NZ -> Prop.
+
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+
+Notation "x < y" := (NZlt x y) : NatIntScope.
+Notation "x <= y" := (NZle x y) : NatIntScope.
+
+Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
+Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
+Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m.
+End NZOrdAxiomsSig.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
new file mode 100644
index 000000000..64cf68489
--- /dev/null
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -0,0 +1,82 @@
+Require Import NZAxioms.
+
+Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
+Open Local Scope NatIntScope.
+
+Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n.
+Proof.
+intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+Qed.
+
+Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step NZE_stepl.
+(* The right step lemma is just the transitivity of NZE *)
+Declare Right Step (proj1 (proj2 NZE_equiv)).
+
+Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
+Proof.
+intros n1 n2 H.
+apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H.
+Qed.
+
+(* The following theorem is useful as an equivalence for proving
+bidirectional induction steps *)
+Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2.
+Proof.
+intros; split.
+apply NZsucc_inj.
+apply NZsucc_wd.
+Qed.
+
+Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m.
+Proof.
+intros; now rewrite NZsucc_inj_wd.
+Qed.
+
+(* We cannot prove that the predecessor is injective, nor that it is
+left-inverse to the successor at this point *)
+
+Section CentralInduction.
+
+Variable A : NZ -> Prop.
+(* FIXME: declaring "A : predicate NZ" leads to the error during the
+declaration of the morphism below because the "predicate NZ" is not
+recognized as a type of function. Maybe it should do "eval hnf" or
+something like this. The same goes for "relation". *)
+
+Hypothesis A_wd : predicate_wd NZE A.
+
+Add Morphism A with signature NZE ==> iff as A_morph.
+Proof A_wd.
+
+Theorem NZcentral_induction :
+  forall z : NZ, A z ->
+    (forall n : NZ, A n <-> A (S n)) ->
+      forall n : NZ, A n.
+Proof.
+intros z Base Step; revert Base; pattern z; apply NZinduction.
+solve_predicate_wd.
+intro; now apply NZinduction.
+intro; pose proof (Step n); tauto.
+Qed.
+
+End CentralInduction.
+
+Tactic Notation "NZinduct" ident(n) :=
+  induction_maker n ltac:(apply NZinduction).
+
+Tactic Notation "NZinduct" ident(n) constr(z) :=
+  induction_maker n ltac:(apply NZcentral_induction with (z := z)).
+
+End NZBasePropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
+
diff --git a/theories/Numbers/NatInt/NZOrdRing.v b/theories/Numbers/NatInt/NZOrdRing.v
new file mode 100644
index 000000000..f35e030e1
--- /dev/null
+++ b/theories/Numbers/NatInt/NZOrdRing.v
@@ -0,0 +1,26 @@
+Require Export NZAxioms.
+Require Import NZTimes.
+
+Module Type NZOrdAxiomsSig.
+Declare Module Export NZAxiomsMod : NZAxiomsSig.
+Open Local Scope NatIntScope.
+
+Parameter Inline NZlt : NZ -> NZ -> Prop.
+Parameter Inline NZle : NZ -> NZ -> Prop.
+
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+
+Notation "x < y" := (NZlt x y) : NatIntScope.
+Notation "x <= y" := (NZle x y) : NatIntScope.
+
+Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
+Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
+Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m.
+End NZOrdAxiomsSig.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZOrder.g b/theories/Numbers/NatInt/NZOrder.g
new file mode 100644
index 000000000..fd7cf608a
--- /dev/null
+++ b/theories/Numbers/NatInt/NZOrder.g
@@ -0,0 +1,219 @@
+Require Export NZBase.
+
+Module Type NZOrderSig.
+Declare Module Export NZBaseMod : NZBaseSig.
+Open Local Scope NatIntScope.
+
+Parameter Inline NZlt : NZ -> NZ -> Prop.
+Parameter Inline NZle : NZ -> NZ -> Prop.
+
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+
+Notation "x < y" := (NZlt x y) : NatIntScope.
+Notation "x <= y" := (NZle x y) : NatIntScope.
+
+Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
+Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
+Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m.
+End NZOrderSig.
+
+Module NZOrderPropFunct (Import NZOrderMod : NZOrderSig).
+Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
+Open Local Scope NatIntScope.
+
+Ltac NZle_intro1 := rewrite NZle_lt_or_eq; left.
+Ltac NZle_intro2 := rewrite NZle_lt_or_eq; right.
+Ltac NZle_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H].
+
+Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
+
+Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z.
+
+Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y.
+
+Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z.
+
+Declare Left  Step NZlt_stepl.
+Declare Right Step NZlt_stepr.
+Declare Left  Step NZle_stepl.
+Declare Right Step NZle_stepr.
+
+Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
+
+Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
+
+Theorem NZle_refl : forall n : NZ, n <= n.
+
+Theorem NZlt_succ_r : forall n : NZ, n < S n.
+
+Theorem NZle_succ_r : forall n : NZ, n <= S n.
+
+Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m.
+
+Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m.
+
+Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
+
+(* The following theorem is a special case of neq_succ_iter_l below,
+but we prove it independently *)
+
+Theorem neq_succ_l : forall n : NZ, S n ~= n.
+
+Theorem nlt_succ_l : forall n : NZ, ~ S n < n.
+
+Theorem nle_succ_l : forall n : NZ, ~ S n <= n.
+
+Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m.
+
+Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m.
+
+Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m.
+
+Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
+
+Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
+
+Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False.
+
+Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
+
+Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
+
+Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
+
+Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
+
+Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p.
+
+Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m.
+
+(** Trichotomy, decidability, and double negation elimination *)
+
+Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
+
+Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n.
+
+Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n.
+
+Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m.
+
+Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
+
+Theorem nle_lt : forall n m : NZ, ~ n <= m <-> m < n.
+
+Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m.
+
+Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
+
+Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n.
+
+(* The difference between integers and natural numbers is that for
+every integer there is a predecessor, which is not true for natural
+numbers. However, for both classes, every number that is bigger than
+some other number has a predecessor. The proof of this fact by regular
+induction does not go through, so we need to use strong
+(course-of-value) induction. *)
+
+Lemma NZlt_exists_pred_strong :
+  forall z n m : NZ, z < m -> m <= n -> exists k : NZ, m == S k /\ z <= k.
+
+Theorem NZlt_exists_pred :
+  forall z n : NZ, z < n -> exists k : NZ, n == S k /\ z <= k.
+
+(** A corollary of having an order is that NZ is infinite *)
+
+(* This section about infinity of NZ relies on the type nat and can be
+safely removed *)
+
+Definition NZsucc_iter (n : nat) (m : NZ) :=
+  nat_rec (fun _ => NZ) m (fun _ l => S l) n.
+
+Theorem NZlt_succ_iter_r :
+  forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m.
+
+Theorem neq_succ_iter_l :
+  forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m.
+
+(* End of the section about the infinity of NZ *)
+
+(** Stronger variant of induction with assumptions n >= 0 (n < 0)
+in the induction step *)
+
+Section Induction.
+
+Variable A : NZ -> Prop.
+Hypothesis A_wd : predicate_wd NZE A.
+
+Add Morphism A with signature NZE ==> iff as A_morph.
+Proof A_wd.
+
+Section Center.
+
+Variable z : NZ. (* A z is the basis of induction *)
+
+Section RightInduction.
+
+Let A' (n : NZ) := forall m : NZ, z <= m -> m < n -> A m.
+
+Add Morphism A' with signature NZE ==> iff as A'_pos_wd.
+Proof.
+unfold A'; solve_predicate_wd.
+Qed.
+
+Theorem right_induction :
+  A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> forall n : NZ, z <= n -> A n.
+
+End RightInduction.
+
+Section LeftInduction.
+
+Let A' (n : NZ) := forall m : NZ, m <= z -> n <= m -> A m.
+
+Add Morphism A' with signature NZE ==> iff as A'_neg_wd.
+Proof.
+unfold A'; solve_predicate_wd.
+Qed.
+
+Theorem NZleft_induction :
+  A z -> (forall n : NZ, n < z -> A (S n) -> A n) -> forall n : NZ, n <= z -> A n.
+
+End LeftInduction.
+
+Theorem central_induction :
+  A z ->
+  (forall n : NZ, z <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n < z  -> A (S n) -> A n) ->
+    forall n : NZ, A n.
+
+End Center.
+
+Theorem induction_0 :
+  A 0 ->
+  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n < 0  -> A (S n) -> A n) ->
+    forall n : NZ, A n.
+
+(** Elimintation principle for < *)
+
+Theorem NZlt_ind : forall (n : NZ),
+  A (S n) ->
+  (forall m : NZ, n < m -> A m -> A (S m)) ->
+   forall m : NZ, n < m -> A m.
+
+(** Elimintation principle for <= *)
+
+Theorem NZle_ind : forall (n : NZ),
+  A n ->
+  (forall m : NZ, n <= m -> A m -> A (S m)) ->
+   forall m : NZ, n <= m -> A m.
+
+End Induction.
+
+End NZOrderPropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
new file mode 100644
index 000000000..f5b757a20
--- /dev/null
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -0,0 +1,538 @@
+Require Import NZAxioms.
+Require Import NZTimes.
+
+Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
+Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod.
+Open Local Scope NatIntScope.
+
+Ltac le_less := rewrite NZle_lt_or_eq; left; try assumption.
+Ltac le_equal := rewrite NZle_lt_or_eq; right; try reflexivity; try assumption.
+Ltac le_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H].
+
+Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Declare Left  Step NZlt_stepl.
+Declare Right Step NZlt_stepr.
+Declare Left  Step NZle_stepl.
+Declare Right Step NZle_stepr.
+
+Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
+Proof.
+intros; now le_less.
+Qed.
+
+Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
+Qed.
+
+Theorem NZle_refl : forall n : NZ, n <= n.
+Proof.
+intro; now le_equal.
+Qed.
+
+Theorem NZlt_succ_r : forall n : NZ, n < S n.
+Proof.
+intro n. rewrite NZlt_succ_le. now le_equal.
+Qed.
+
+Theorem NZle_succ_r : forall n : NZ, n <= S n.
+Proof.
+intro; le_less; apply NZlt_succ_r.
+Qed.
+
+Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m.
+Proof.
+intros. rewrite NZlt_succ_le. now le_less.
+Qed.
+
+Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m.
+Proof.
+intros n m H; rewrite <- NZlt_succ_le in H; now le_less.
+Qed.
+
+Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
+Proof.
+intros n m; rewrite NZle_lt_or_eq. now rewrite NZlt_succ_le.
+Qed.
+
+(* The following theorem is a special case of neq_succ_iter_l below,
+but we prove it independently *)
+
+Theorem NZneq_succ_l : forall n : NZ, S n ~= n.
+Proof.
+intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1.
+false_hyp H1 NZlt_irrefl.
+Qed.
+
+Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n.
+Proof.
+intros n H; apply NZlt_lt_succ in H. false_hyp H NZlt_irrefl.
+Qed.
+
+Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n.
+Proof.
+intros n H; le_elim H.
+false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l.
+Qed.
+
+Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m.
+Proof.
+intro n; NZinduct m n.
+rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l.
+intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ.
+rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m).
+rewrite or_cancel_r.
+apply NZlt_neq.
+intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l.
+reflexivity.
+Qed.
+
+Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m.
+Proof.
+intros n m H; apply <- NZlt_le_succ; now le_less.
+Qed.
+
+Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m.
+Proof.
+intros n m H; le_less; now apply <- NZlt_le_succ.
+Qed.
+
+Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
+Proof.
+intros n m. rewrite NZlt_le_succ. symmetry. apply NZlt_succ_le.
+Qed.
+
+Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
+Proof.
+intros n m. do 2 rewrite NZle_lt_or_eq.
+rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False.
+Proof.
+intros n m; NZinduct n m.
+intros H _; false_hyp H NZlt_irrefl.
+intro n; split; intros H H1 H2.
+apply NZlt_succ_lt in H1. apply -> NZlt_succ_le in H2. le_elim H2.
+now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
+apply NZlt_lt_succ in H2. apply -> NZlt_le_succ in H1. le_elim H1.
+now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl.
+Qed.
+
+Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
+Proof.
+intros n m; unfold not; apply NZlt_lt_false.
+Qed.
+
+Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
+Proof.
+intros n m p; NZinduct p m.
+intros _ H; false_hyp H NZlt_irrefl.
+intro p. do 2 rewrite NZlt_succ_le.
+split; intros H H1 H2.
+le_less; le_elim H2; [now apply H | now rewrite H2 in H1].
+assert (n <= p) as H3. apply H. assumption. now le_less.
+le_elim H3. assumption. rewrite <- H3 in H2. elimtype False.
+now apply (NZlt_lt_false n m).
+Qed.
+
+Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+le_elim H2. le_less; now apply NZlt_trans with (m := m).
+le_less; now rewrite <- H2. now rewrite H1.
+Qed.
+
+Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+now apply NZlt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+now apply NZlt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m.
+Proof.
+intros n m H1 H2; now (le_elim H1; le_elim H2);
+[elimtype False; apply (NZlt_lt_false n m) | | |].
+Qed.
+
+(** Trichotomy, decidability, and double negation elimination *)
+
+Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
+Proof.
+intros n m; NZinduct n m.
+right; now left.
+intro n; rewrite NZlt_succ_le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto.
+rewrite <- (NZle_lt_or_eq (S n) m). symmetry (n == m).
+stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle_lt_or_eq.
+apply or_iff_compat_r. apply NZlt_le_succ.
+Qed.
+
+Theorem NZE_dec : forall n m : NZ, n == m \/ n ~= m.
+Proof.
+intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
+right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
+now left.
+right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
+Qed.
+
+Theorem NZE_dne : forall n m, ~ ~ n == m <-> n == m.
+Proof.
+intros n m; split; intro H.
+destruct (NZE_dec n m) as [H1 | H1].
+assumption. false_hyp H1 H.
+intro H1; now apply H1.
+Qed.
+
+Theorem NZneq_lt_or_gt : forall n m : NZ, n ~= m <-> n < m \/ m < n.
+Proof.
+intros n m; split.
+pose proof (NZlt_trichotomy n m); tauto.
+intros H H1; destruct H as [H | H]; rewrite H1 in H; false_hyp H NZlt_irrefl.
+Qed.
+
+Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n.
+Proof.
+intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
+left; now le_less. left; now le_equal. now right.
+Qed.
+
+Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n.
+Proof.
+intros n m. split; intro H; [intro H1 |].
+eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl.
+destruct (NZle_lt_dec n m) as [H1 | H1].
+assumption. false_hyp H1 H.
+Qed.
+
+Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m.
+Proof.
+intros n m; destruct (NZle_lt_dec m n);
+[right; now apply -> NZle_nlt | now left].
+Qed.
+
+Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
+Proof.
+intros n m; split; intro H;
+[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+intro H1; false_hyp H H1].
+Qed.
+
+Theorem NZnle_lt : forall n m : NZ, ~ n <= m <-> m < n.
+Proof.
+intros n m. rewrite NZle_nlt. apply NZlt_dne.
+Qed.
+
+Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m.
+Proof.
+intros n m; destruct (NZle_lt_dec n m);
+[now left | right; now apply <- NZnle_lt].
+Qed.
+
+Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
+Proof.
+intros n m; split; intro H;
+[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+intro H1; false_hyp H H1].
+Qed.
+
+Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n.
+Proof.
+intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_lt.
+Qed.
+
+(* The difference between integers and natural numbers is that for
+every integer there is a predecessor, which is not true for natural
+numbers. However, for both classes, every number that is bigger than
+some other number has a predecessor. The proof of this fact by regular
+induction does not go through, so we need to use strong
+(course-of-value) induction. *)
+
+Lemma NZlt_exists_pred_strong :
+  forall z n m : NZ, z < m -> m <= n -> exists k : NZ, m == S k /\ z <= k.
+Proof.
+intro z; NZinduct n z.
+intros m H1 H2; apply <- NZnle_lt in H1; false_hyp H2 H1.
+intro n; split; intros IH m H1 H2.
+apply -> NZle_succ_le_or_eq_succ in H2; destruct H2 as [H2 | H2].
+now apply IH. exists n. now split; [| rewrite <- NZlt_succ_le; rewrite <- H2].
+apply IH. assumption. now apply NZle_le_succ.
+Qed.
+
+Theorem NZlt_exists_pred :
+  forall z n : NZ, z < n -> exists k : NZ, n == S k /\ z <= k.
+Proof.
+intros z n H; apply NZlt_exists_pred_strong with (z := z) (n := n).
+assumption. apply NZle_refl.
+Qed.
+
+(** A corollary of having an order is that NZ is infinite *)
+
+(* This section about infinity of NZ relies on the type nat and can be
+safely removed *)
+
+Definition NZsucc_iter (n : nat) (m : NZ) :=
+  nat_rec (fun _ => NZ) m (fun _ l => S l) n.
+
+Theorem NZlt_succ_iter_r :
+  forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m.
+Proof.
+intros n m; induction n as [| n IH]; simpl in *.
+apply NZlt_succ_r. now apply NZlt_lt_succ.
+Qed.
+
+Theorem NZneq_succ_iter_l :
+  forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m.
+Proof.
+intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1.
+false_hyp H1 NZlt_irrefl.
+Qed.
+
+(* End of the section about the infinity of NZ *)
+
+(** Stronger variant of induction with assumptions n >= 0 (n < 0)
+in the induction step *)
+
+Section Induction.
+
+Variable A : NZ -> Prop.
+Hypothesis A_wd : predicate_wd NZE A.
+
+Add Morphism A with signature NZE ==> iff as A_morph.
+Proof A_wd.
+
+Section Center.
+
+Variable z : NZ. (* A z is the basis of induction *)
+
+Section RightInduction.
+
+Let A' (n : NZ) := forall m : NZ, z <= m -> m < n -> A m.
+Let right_step :=   forall n : NZ, z <= n -> A n -> A (S n).
+Let right_step' :=  forall n : NZ, z <= n -> A' n -> A n.
+Let right_step'' := forall n : NZ, A' n <-> A' (S n).
+
+Lemma NZrs_rs' :  A z -> right_step -> right_step'.
+Proof.
+intros Az RS n H1 H2.
+le_elim H1. apply NZlt_exists_pred in H1. destruct H1 as [k [H3 H4]].
+rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_r]].
+rewrite <- H1; apply Az.
+Qed.
+
+Lemma NZrs'_rs'' : right_step' -> right_step''.
+Proof.
+intros RS' n; split; intros H1 m H2 H3.
+apply -> NZlt_succ_le in H3; le_elim H3;
+[now apply H1 | rewrite H3 in *; now apply RS'].
+apply H1; [assumption | now apply NZlt_lt_succ].
+Qed.
+
+Lemma NZrbase : A' z.
+Proof.
+intros m H1 H2. apply -> NZle_nlt in H1. false_hyp H2 H1.
+Qed.
+
+Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n.
+Proof.
+intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_r].
+Qed.
+
+Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n.
+Proof.
+intro RS'; apply NZA'A_right; unfold A'; NZinduct n z;
+[apply NZrbase | apply NZrs'_rs''; apply RS'].
+Qed.
+
+Theorem NZright_induction : A z -> right_step -> forall n : NZ, z <= n -> A n.
+Proof.
+intros Az RS; apply NZstrong_right_induction; now apply NZrs_rs'.
+Qed.
+
+End RightInduction.
+
+Section LeftInduction.
+
+Let A' (n : NZ) := forall m : NZ, m <= z -> n <= m -> A m.
+Let left_step :=   forall n : NZ, n < z -> A (S n) -> A n.
+Let left_step' :=  forall n : NZ, n <= z -> A' (S n) -> A n.
+Let left_step'' := forall n : NZ, A' n <-> A' (S n).
+
+Lemma NZls_ls' :  A z -> left_step -> left_step'.
+Proof.
+intros Az LS n H1 H2. le_elim H1.
+apply LS; [assumption | apply H2; [now apply -> NZlt_le_succ | now le_equal]].
+rewrite H1; apply Az.
+Qed.
+
+Lemma NZls'_ls'' : left_step' -> left_step''.
+Proof.
+intros LS' n; split; intros H1 m H2 H3.
+apply NZle_succ_le in H3. now apply H1.
+le_elim H3.
+apply -> NZlt_le_succ in H3. now apply H1.
+rewrite <- H3 in *; now apply LS'.
+Qed.
+
+Lemma NZlbase : A' (S z).
+Proof.
+intros m H1 H2. apply <- NZlt_le_succ in H2.
+apply -> NZle_nlt in H1. false_hyp H2 H1.
+Qed.
+
+Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n.
+Proof.
+intros H1 n H2. apply H1 with (n := n); [assumption | now le_equal].
+Qed.
+
+Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n.
+Proof.
+intro LS'; apply NZA'A_left; unfold A'; NZinduct n (S z);
+[apply NZlbase | apply NZls'_ls''; apply LS'].
+Qed.
+
+Theorem NZleft_induction : A z -> left_step -> forall n : NZ, n <= z -> A n.
+Proof.
+intros Az LS; apply NZstrong_left_induction; now apply NZls_ls'.
+Qed.
+
+End LeftInduction.
+
+Theorem NZorder_induction :
+  A z ->
+  (forall n : NZ, z <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n < z  -> A (S n) -> A n) ->
+    forall n : NZ, A n.
+Proof.
+intros Az RS LS n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+now apply NZleft_induction; [| | le_less].
+now rewrite H.
+now apply NZright_induction; [| | le_less].
+Qed.
+
+Theorem NZright_induction' :
+  (forall n : NZ, n <= z -> A n) ->
+  (forall n : NZ, z <= n -> A n -> A (S n)) ->
+    forall n : NZ, A n.
+Proof.
+intros L R n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply L; now le_less.
+apply L; now le_equal.
+apply NZright_induction. apply L; now le_equal. assumption. now le_less.
+Qed.
+
+Theorem NZstrong_right_induction' :
+  (forall n : NZ, n <= z -> A n) ->
+  (forall n : NZ, z <= n -> (forall m : NZ, z <= m -> m < n -> A m) -> A n) ->
+    forall n : NZ, A n.
+Proof.
+intros L R n.
+destruct (NZlt_trichotomy n z) as [H | [H | H]].
+apply L; now le_less.
+apply L; now le_equal.
+apply NZstrong_right_induction. assumption. now le_less.
+Qed.
+
+End Center.
+
+Theorem NZorder_induction_0 :
+  A 0 ->
+  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n < 0  -> A (S n) -> A n) ->
+    forall n : NZ, A n.
+Proof (NZorder_induction 0).
+
+(** Elimintation principle for < *)
+
+Theorem NZlt_ind : forall (n : NZ),
+  A (S n) ->
+  (forall m : NZ, n < m -> A m -> A (S m)) ->
+   forall m : NZ, n < m -> A m.
+Proof.
+intros n H1 H2 m H3.
+apply NZright_induction with (S n); [assumption | | now apply -> NZlt_le_succ].
+intros; apply H2; try assumption. now apply <- NZlt_le_succ.
+Qed.
+
+(** Elimintation principle for <= *)
+
+Theorem NZle_ind : forall (n : NZ),
+  A n ->
+  (forall m : NZ, n <= m -> A m -> A (S m)) ->
+   forall m : NZ, n <= m -> A m.
+Proof.
+intros n H1 H2 m H3.
+now apply NZright_induction with n.
+Qed.
+
+End Induction.
+
+Tactic Notation "NZord_induct" ident(n) :=
+  induction_maker n ltac:(apply NZorder_induction_0).
+
+Tactic Notation "NZord_induct" ident(n) constr(z) :=
+  induction_maker n ltac:(apply NZorder_induction with z).
+
+Section WF.
+
+Variable z : NZ.
+
+Let R (n m : NZ) := z <= n /\ n < m.
+
+Add Morphism R with signature NZE ==> NZE ==> iff as R_wd.
+Proof.
+intros x1 x2 H1 x3 x4 H2; unfold R; rewrite H1; now rewrite H2.
+Qed.
+
+Lemma NZAcc_lt_wd : predicate_wd NZE (Acc R).
+Proof.
+unfold predicate_wd, fun_wd.
+intros x1 x2 H; split; intro H1; destruct H1 as [H2];
+constructor; intros; apply H2; now (rewrite H || rewrite <- H).
+Qed.
+
+Theorem NZlt_wf : well_founded R.
+Proof.
+unfold well_founded.
+apply NZstrong_right_induction' with (z := z).
+apply NZAcc_lt_wd.
+intros n H; constructor; intros y [H1 H2].
+apply <- NZnle_lt in H2. elim H2. now apply NZle_trans with z.
+intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
+Qed.
+
+End WF.
+
+End NZOrderPropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZOrder1.v b/theories/Numbers/NatInt/NZOrder1.v
new file mode 100644
index 000000000..6a15ddc6a
--- /dev/null
+++ b/theories/Numbers/NatInt/NZOrder1.v
@@ -0,0 +1,423 @@
+Require Export NZBase.
+
+Module Type NZOrderSig.
+Declare Module Export NZBaseMod : NZBaseSig.
+
+Parameter Inline NZlt : NZ -> NZ -> Prop.
+Parameter Inline NZle : NZ -> NZ -> Prop.
+
+Axiom NZlt_wd : rel_wd NZE NZE NZlt.
+Axiom NZle_wd : rel_wd NZE NZE NZle.
+
+Notation "x < y" := (NZlt x y).
+Notation "x <= y" := (NZle x y).
+
+Axiom NZle__lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
+Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
+Axiom NZlt_succ__le : forall n m : NZ, n < S m <-> n <= m.
+End NZOrderSig.
+
+Module NZOrderPropFunct (Import NZOrderMod : NZOrderSig).
+Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
+
+Ltac NZle_intro1 := rewrite NZle__lt_or_eq; left.
+Ltac NZle_intro2 := rewrite NZle__lt_or_eq; right.
+Ltac NZle_elim H := rewrite NZle__lt_or_eq in H; destruct H as [H | H].
+
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_morph.
+Proof.
+exact NZlt_wd.
+Qed.
+
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_morph.
+Proof.
+exact NZle_wd.
+Qed.
+
+Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z.
+Proof.
+intros x y z H1 H2; now rewrite <- H2.
+Qed.
+
+Declare Left  Step NZlt_stepl.
+Declare Right Step NZlt_stepr.
+Declare Left  Step NZle_stepl.
+Declare Right Step NZle_stepr.
+
+Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
+Proof.
+intros; now NZle_intro1.
+Qed.
+
+Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
+Qed.
+
+Theorem NZle_refl : forall n : NZ, n <= n.
+Proof.
+intro; now NZle_intro2.
+Qed.
+
+Theorem NZlt_succ_r : forall n : NZ, n < S n.
+Proof.
+intro n. rewrite NZlt_succ__le. now NZle_intro2.
+Qed.
+
+Theorem NZle_succ_r : forall n : NZ, n <= S n.
+Proof.
+intro; NZle_intro1; apply NZlt_succ_r.
+Qed.
+
+Theorem NZlt__lt_succ : forall n m : NZ, n < m -> n < S m.
+Proof.
+intros. rewrite NZlt_succ__le. now NZle_intro1.
+Qed.
+
+Theorem NZle__le_succ : forall n m : NZ, n <= m -> n <= S m.
+Proof.
+intros n m H; rewrite <- NZlt_succ__le in H; now NZle_intro1.
+Qed.
+
+Theorem NZle_succ__le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
+Proof.
+intros n m; rewrite NZle__lt_or_eq. now rewrite NZlt_succ__le.
+Qed.
+
+(** A corollary of having an order is that NZ is infinite *)
+
+(* This section about infinity of NZ relies on the type nat and can be
+safely removed *)
+
+Definition succ_iter (n : nat) (m : NZ) :=
+  nat_rec (fun _ => NZ) m (fun _ l => S l) n.
+
+Theorem NZlt_succ_iter_r :
+  forall (n : nat) (m : NZ), m < succ_iter (Datatypes.S n) m.
+Proof.
+intros n m; induction n as [| n IH]; simpl in *.
+apply NZlt_succ_r. now apply NZlt__lt_succ.
+Qed.
+
+Theorem NZneq_succ_iter_l :
+  forall (n : nat) (m : NZ), succ_iter (Datatypes.S n) m ~= m.
+Proof.
+intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1.
+false_hyp H1 NZlt_irrefl.
+Qed.
+
+(* End of the section about the infinity of NZ *)
+
+(* The following theorem is a special case of NZneq_succ_iter_l, but we
+prove it independently *)
+
+Theorem NZneq_succ_l : forall n : NZ, S n ~= n.
+Proof.
+intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1.
+false_hyp H1 NZlt_irrefl.
+Qed.
+
+Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n.
+Proof.
+intros n H; apply NZlt__lt_succ in H. false_hyp H NZlt_irrefl.
+Qed.
+
+Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n.
+Proof.
+intros n H; NZle_elim H.
+false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l.
+Qed.
+
+Theorem NZlt__le_succ : forall n m : NZ, n < m <-> S n <= m.
+Proof.
+intro n; NZinduct_center m n.
+rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l.
+intro m. rewrite NZlt_succ__le. rewrite NZle_succ__le_or_eq_succ.
+rewrite NZsucc_inj_wd. rewrite (NZle__lt_or_eq n m).
+rewrite or_cancel_r.
+apply NZlt_neq.
+intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l.
+reflexivity.
+Qed.
+
+Theorem NZlt_succ__lt : forall n m : NZ, S n < m -> n < m.
+Proof.
+intros n m H; apply <- NZlt__le_succ; now NZle_intro1.
+Qed.
+
+Theorem NZle_succ__le : forall n m : NZ, S n <= m -> n <= m.
+Proof.
+intros n m H; NZle_intro1; now apply <- NZlt__le_succ.
+Qed.
+
+Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
+Proof.
+intros n m. rewrite NZlt__le_succ. symmetry. apply NZlt_succ__le.
+Qed.
+
+Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
+Proof.
+intros n m. do 2 rewrite NZle__lt_or_eq.
+rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False.
+Proof.
+intros n m; NZinduct_center n m.
+intros H _; false_hyp H NZlt_irrefl.
+intro n; split; intros H H1 H2.
+apply NZlt_succ__lt in H1. apply -> NZlt_succ__le in H2. NZle_elim H2.
+now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
+apply NZlt__lt_succ in H2. apply -> NZlt__le_succ in H1. NZle_elim H1.
+now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl.
+Qed.
+
+Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
+Proof.
+intros n m; unfold not; apply NZlt_lt_false.
+Qed.
+
+Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
+Proof.
+intros n m p; NZinduct_center p m.
+intros _ H; false_hyp H NZlt_irrefl.
+intro p. do 2 rewrite NZlt_succ__le.
+split; intros H H1 H2.
+NZle_intro1; NZle_elim H2; [now apply H | now rewrite H2 in H1].
+assert (n <= p) as H3. apply H. assumption. now NZle_intro1.
+NZle_elim H3. assumption. rewrite <- H3 in H2. elimtype False.
+now apply (NZlt_lt_false n m).
+Qed.
+
+Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p H1 H2; NZle_elim H1.
+NZle_elim H2. NZle_intro1; now apply NZlt_trans with (m := m).
+NZle_intro1; now rewrite <- H2. now rewrite H1.
+Qed.
+
+Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; NZle_elim H1.
+now apply NZlt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; NZle_elim H2.
+now apply NZlt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem NZle_antisym : forall n m : NZ, n <= m -> m <= n -> n == m.
+Proof.
+intros n m H1 H2; now (NZle_elim H1; NZle_elim H2);
+[elimtype False; apply (NZlt_lt_false n m) | | |].
+Qed.
+
+(** Trichotomy, decidability, and double negation elimination *)
+
+Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
+Proof.
+intros n m; NZinduct_center n m.
+right; now left.
+intro n; rewrite NZlt_succ__le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto.
+rewrite <- (NZle__lt_or_eq (S n) m). symmetry (n == m).
+stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle__lt_or_eq.
+apply or_iff_compat_r. apply NZlt__le_succ.
+Qed.
+
+Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n.
+Proof.
+intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
+left; now NZle_intro1. left; now NZle_intro2. now right.
+Qed.
+
+Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n.
+Proof.
+intros n m. split; intro H; [intro H1 |].
+eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl.
+destruct (NZle_lt_dec n m) as [H1 | H1].
+assumption. false_hyp H1 H.
+Qed.
+
+Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m.
+Proof.
+intros n m; destruct (NZle_lt_dec m n);
+[right; now apply -> NZle_nlt | now left].
+Qed.
+
+Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
+Proof.
+intros n m; split; intro H;
+[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+intro H1; false_hyp H H1].
+Qed.
+
+Theorem NZnle_lt : forall n m : NZ, ~ n <= m <-> m < n.
+Proof.
+intros n m. rewrite NZle_nlt. apply NZlt_dne.
+Qed.
+
+Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m.
+Proof.
+intros n m; destruct (NZle_lt_dec n m);
+[now left | right; now apply <- NZnle_lt].
+Qed.
+
+Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
+Proof.
+intros n m; split; intro H;
+[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+intro H1; false_hyp H H1].
+Qed.
+
+Theorem NZlt__nlt_succ : forall n m : NZ, n < m <-> ~ m < S n.
+Proof.
+intros n m; rewrite NZlt_succ__le; symmetry; apply NZnle_lt.
+Qed.
+
+(** Stronger variant of induction with assumptions n >= 0 (n <= 0)
+in the induction step *)
+
+Section Induction.
+
+Variable A : Z -> Prop.
+Hypothesis Q_wd : predicate_wd NZE A.
+
+Add Morphism A with signature NZE ==> iff as Q_morph.
+Proof Q_wd.
+
+Section Center.
+
+Variable z : Z. (* A z is the basis of induction *)
+
+Section RightInduction.
+
+Let Q' := fun n : Z => forall m : NZ, z <= m -> m < n -> A m.
+
+Add Morphism Q' with signature NZE ==> iff as Q'_pos_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem NZright_induction :
+  A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> forall n : NZ, z <= n -> A n.
+Proof.
+intros Qz QS k k_ge_z.
+assert (H : forall n : NZ, 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 NZlt_succ in H3; Zle_elim H3. now apply IH.
+Zle_elim H2. rewrite_succ_pred m.
+apply QS. now apply -> lt_n_m_pred. apply IH. now apply -> lt_n_m_pred.
+rewrite H3; apply NZlt_pred_l. now rewrite <- H2.
+intros n IH m H2 H3. apply IH. assumption. now apply lt_n_predm.
+pose proof (H (S k)) as H1; unfold Q' in H1. apply H1.
+apply k_ge_z. apply NZlt_succ_r.
+Qed.
+
+End RightInduction.
+
+Section LeftInduction.
+
+Let Q' := fun n : Z => forall m : NZ, m <= z -> n < m -> A m.
+
+Add Morphism Q' with signature NZE ==> iff as Q'_neg_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem NZleft_induction :
+  A z -> (forall n : NZ, n <= z -> A n -> A (P n)) -> forall n : NZ, n <= z -> A n.
+Proof.
+intros Qz QP k k_le_z.
+assert (H : forall n : NZ, 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_succ__lt.
+intros n IH m H2 H3.
+rewrite NZlt_pred in H3; Zle_elim H3. now apply IH.
+Zle_elim H2. rewrite_pred_succ m.
+apply QP. now apply -> lt_n_m_succ. apply IH. now apply -> lt_n_m_succ.
+rewrite H3; apply NZlt_succ_r. now rewrite H2.
+pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
+apply k_le_z. apply NZlt_pred_l.
+Qed.
+
+End LeftInduction.
+
+Theorem NZinduction_ord_n :
+  A z ->
+  (forall n : NZ, z <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n <= z -> A n -> A (P n)) ->
+    forall n : NZ, A n.
+Proof.
+intros Qz QS QP n.
+destruct (lt_total n z) as [H | [H | H]].
+now apply left_induction; [| | Zle_intro1].
+now rewrite H.
+now apply right_induction; [| | Zle_intro1].
+Qed.
+
+End Center.
+
+Theorem NZinduction_ord :
+  A 0 ->
+  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
+  (forall n : NZ, n <= 0 -> A n -> A (P n)) ->
+    forall n : NZ, A n.
+Proof (induction_ord_n 0).
+
+Theorem NZlt_ind : forall (n : Z),
+  A (S n) ->
+  (forall m : Z, n < m -> A m -> A (S m)) ->
+   forall m : Z, n < m -> A 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_succ.
+now apply -> lt_n_m_succ.
+Qed.
+
+Theorem NZle_ind : forall (n : Z),
+  A n ->
+  (forall m : Z, n <= m -> A m -> A (S m)) ->
+   forall m : Z, n <= m -> A 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.predicate_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | | |].
+
+End ZOrderProperties.
+
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v
new file mode 100644
index 000000000..d333274ba
--- /dev/null
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -0,0 +1,91 @@
+Require Import NZAxioms.
+Require Import NZBase.
+
+Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig).
+Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod.
+Open Local Scope NatIntScope.
+
+(** If H1 : t1 == u1 and H2 : t2 == u2 then "add_equations H1 H2 as H3"
+adds the hypothesis H3 : t1 + t2 == u1 + u2 *)
+Tactic Notation "add_equations" constr(H1) constr(H2) "as" ident(H3) :=
+match (type of H1) with
+| ?t1 == ?u1 => match (type of H2) with
+              | ?t2 == ?u2 => assert (H3 : t1 + t2 == u1 + u2); [now apply NZplus_wd |]
+              | _ => fail 2 ":" H2 "is not an equation"
+              end
+| _ => fail 1 ":" H1 "is not an equation"
+end.
+
+Theorem NZplus_0_r : forall n : NZ, n + 0 == n.
+Proof.
+NZinduct n. now rewrite NZplus_0_l.
+intro. rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZplus_succ_r : forall n m : NZ, n + S m == S (n + m).
+Proof.
+intros n m; NZinduct n.
+now do 2 rewrite NZplus_0_l.
+intro. repeat rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZplus_comm : forall n m : NZ, n + m == m + n.
+Proof.
+intros n m; NZinduct n.
+rewrite NZplus_0_l; now rewrite NZplus_0_r.
+intros n. rewrite NZplus_succ_l; rewrite NZplus_succ_r. now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZplus_1_l : forall n : NZ, 1 + n == S n.
+Proof.
+intro n; rewrite NZplus_succ_l; now rewrite NZplus_0_l.
+Qed.
+
+Theorem NZplus_1_r : forall n : NZ, n + 1 == S n.
+Proof.
+intro n; rewrite NZplus_comm; apply NZplus_1_l.
+Qed.
+
+Theorem NZplus_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p.
+Proof.
+intros n m p; NZinduct n.
+now do 2 rewrite NZplus_0_l.
+intro. do 3 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZplus_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q).
+Proof.
+intros n m p q.
+rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_comm m (p + q)).
+rewrite <- (NZplus_assoc p q m). rewrite (NZplus_assoc n p (q + m)).
+now rewrite (NZplus_comm q m).
+Qed.
+
+Theorem NZplus_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p).
+Proof.
+intros n m p q.
+rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_assoc m p q).
+rewrite (NZplus_comm (m + p) q). now rewrite <- (NZplus_assoc n q (m + p)).
+Qed.
+
+Theorem NZplus_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m.
+Proof.
+intros n m p; NZinduct p.
+now do 2 rewrite NZplus_0_l.
+intro p. do 2 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+Qed.
+
+Theorem NZplus_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m.
+Proof.
+intros n m p. rewrite (NZplus_comm n p); rewrite (NZplus_comm m p).
+apply NZplus_cancel_l.
+Qed.
+
+End NZPlusPropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
new file mode 100644
index 000000000..f43b549e2
--- /dev/null
+++ b/theories/Numbers/NatInt/NZPlusOrder.v
@@ -0,0 +1,73 @@
+Require Export NZPlus.
+Require Export NZOrder.
+
+Module NZPlusOrderPropFunct
+  (Import NZPlusMod : NZPlusSig)
+  (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod).
+
+Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
+Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
+Open Local Scope NatIntScope.
+
+Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
+Proof.
+intros n m p; NZinduct p.
+now do 2 rewrite NZplus_0_l.
+intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
+Qed.
+
+Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
+Proof.
+intros n m p.
+rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
+Qed.
+
+Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_trans with (m + p);
+[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
+Qed.
+
+Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; NZinduct p.
+now do 2 rewrite NZplus_0_l.
+intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
+Qed.
+
+Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p.
+rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
+Qed.
+
+Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZle_trans with (m + p);
+[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
+Qed.
+
+Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_le_trans with (m + p);
+[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
+Qed.
+
+Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZle_lt_trans with (m + p);
+[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
+Qed.
+
+End NZPlusOrderPropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZRing.v b/theories/Numbers/NatInt/NZRing.v
new file mode 100644
index 000000000..2425224b8
--- /dev/null
+++ b/theories/Numbers/NatInt/NZRing.v
@@ -0,0 +1,45 @@
+Require Export NumPrelude.
+
+Module Type NZRingSig.
+
+Parameter Inline NZ : Set.
+Parameter Inline NZE : NZ -> NZ -> Prop.
+Parameter Inline NZ0 : NZ.
+Parameter Inline NZsucc : NZ -> NZ.
+Parameter Inline NZplus : NZ -> NZ -> NZ.
+Parameter Inline NZtimes : NZ -> NZ -> NZ.
+
+Axiom NZE_equiv : equiv NZ NZE.
+Add Relation NZ NZE
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
+
+Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+
+Delimit Scope NatIntScope with NatInt.
+Open Local Scope NatIntScope.
+Notation "x == y"  := (NZE x y) (at level 70) : NatIntScope.
+Notation "x ~= y" := (~ NZE x y) (at level 70) : NatIntScope.
+Notation "0" := NZ0 : NatIntScope.
+Notation "'S'" := NZsucc.
+Notation "1" := (S 0) : NatIntScope.
+Notation "x + y" := (NZplus x y) : NatIntScope.
+Notation "x * y" := (NZtimes x y) : NatIntScope.
+
+Axiom NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
+
+Axiom NZinduction :
+  forall A : NZ -> Prop, predicate_wd NZE A ->
+    A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
+
+Axiom NZplus_0_l : forall n : NZ, 0 + n == n.
+Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+
+Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0.
+Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+
+End NZRingSig.
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
new file mode 100644
index 000000000..ca78ced69
--- /dev/null
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -0,0 +1,74 @@
+Require Import NZAxioms.
+Require Import NZPlus.
+
+Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig).
+Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod.
+Open Local Scope NatIntScope.
+
+Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0.
+Proof.
+NZinduct n.
+now rewrite NZtimes_0_r.
+intro. rewrite NZtimes_succ_r. now rewrite NZplus_0_r.
+Qed.
+
+Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m.
+Proof.
+intros n m; NZinduct m.
+do 2 rewrite NZtimes_0_r; now rewrite NZplus_0_l.
+intro m. do 2 rewrite NZtimes_succ_r. do 2 rewrite NZplus_succ_r.
+rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) n m).
+rewrite (NZplus_comm n m). rewrite NZplus_assoc.
+now rewrite NZplus_cancel_r.
+Qed.
+
+Theorem NZtimes_comm : forall n m : NZ, n * m == m * n.
+Proof.
+intros n m; NZinduct n.
+rewrite NZtimes_0_l; now rewrite NZtimes_0_r.
+intro. rewrite NZtimes_succ_l; rewrite NZtimes_succ_r. now rewrite NZplus_cancel_r.
+Qed.
+
+Theorem NZtimes_plus_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.
+Proof.
+intros n m p; NZinduct n.
+rewrite NZtimes_0_l. now do 2 rewrite NZplus_0_l.
+intro n. rewrite NZplus_succ_l. do 2 rewrite NZtimes_succ_l.
+rewrite <- (NZplus_assoc (n * p) p (m * p)).
+rewrite (NZplus_comm p (m * p)). rewrite (NZplus_assoc (n * p) (m * p) p).
+now rewrite NZplus_cancel_r.
+Qed.
+
+Theorem NZtimes_plus_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.
+Proof.
+intros n m p.
+rewrite (NZtimes_comm n (m + p)). rewrite (NZtimes_comm n m).
+rewrite (NZtimes_comm n p). apply NZtimes_plus_distr_r.
+Qed.
+
+Theorem NZtimes_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.
+Proof.
+intros n m p; NZinduct n.
+now do 3 rewrite NZtimes_0_l.
+intro n. do 2 rewrite NZtimes_succ_l. rewrite NZtimes_plus_distr_r.
+now rewrite NZplus_cancel_r.
+Qed.
+
+Theorem NZtimes_1_l : forall n : NZ, 1 * n == n.
+Proof.
+intro n. rewrite NZtimes_succ_l; rewrite NZtimes_0_l. now rewrite NZplus_0_l.
+Qed.
+
+Theorem NZtimes_1_r : forall n : NZ, n * 1 == n.
+Proof.
+intro n; rewrite NZtimes_comm; apply NZtimes_1_l.
+Qed.
+
+End NZTimesPropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
new file mode 100644
index 000000000..95275f8c0
--- /dev/null
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -0,0 +1,315 @@
+Require Import NZAxioms.
+Require Import NZOrder.
+
+Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
+Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod.
+Open Local Scope NatIntScope.
+
+(** Addition and order *)
+
+Theorem NZplus_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m.
+Proof.
+intros n m p; NZinduct p.
+now do 2 rewrite NZplus_0_l.
+intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
+Qed.
+
+Theorem NZplus_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p.
+Proof.
+intros n m p.
+rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
+Qed.
+
+Theorem NZplus_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_trans with (m + p);
+[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
+Qed.
+
+Theorem NZplus_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; NZinduct p.
+now do 2 rewrite NZplus_0_l.
+intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
+Qed.
+
+Theorem NZplus_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p.
+rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
+Qed.
+
+Theorem NZplus_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZle_trans with (m + p);
+[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
+Qed.
+
+Theorem NZplus_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_le_trans with (m + p);
+[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
+Qed.
+
+Theorem NZplus_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply NZle_lt_trans with (m + p);
+[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
+Qed.
+
+Theorem NZplus_le_lt_mono_opp : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q.
+Proof.
+intros n m p q H1 H2. destruct (NZle_lt_dec q p); [| assumption].
+pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_lt in H2.
+false_hyp H3 H2.
+Qed.
+
+Theorem NZplus_lt_inv : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q.
+Proof.
+intros n m p q H;
+destruct (NZle_lt_dec p n) as [H1 | H1].
+destruct (NZle_lt_dec q m) as [H2 | H2].
+pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_nlt in H3.
+false_hyp H H3.
+now right. now left.
+Qed.
+
+Theorem NZplus_lt_inv_0 : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
+Proof.
+intros n m H; apply NZplus_lt_inv; now rewrite NZplus_0_l.
+Qed.
+
+Theorem NZplus_gt_inv_0 : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Proof.
+intros n m H; apply NZplus_lt_inv; now rewrite NZplus_0_l.
+Qed.
+
+(** Multiplication and order *)
+
+Theorem NZtimes_lt_pred :
+  forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Proof.
+intros p q n m H. rewrite <- H. do 2 rewrite NZtimes_succ_l.
+rewrite <- (NZplus_assoc (p * n) n m).
+rewrite <- (NZplus_assoc (p * m) m n).
+rewrite (NZplus_comm n m). now rewrite <- NZplus_lt_mono_r.
+Qed.
+
+Theorem NZtimes_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m).
+Proof.
+NZord_induct p.
+intros n m H; false_hyp H NZlt_irrefl.
+intros p H IH n m H1. do 2 rewrite NZtimes_succ_l.
+le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m).
+intros n1 m1 H2. apply NZplus_lt_mono; [now apply -> IH | assumption].
+split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
+apply <- NZle_nlt in H3. le_elim H3.
+apply NZlt_asymm in H2. apply H2. now apply LR.
+rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
+rewrite <- H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
+intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1.
+Qed.
+
+Theorem NZtimes_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p).
+Proof.
+intros p n m.
+rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p). now apply NZtimes_lt_mono_pos_l.
+Qed.
+
+Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n).
+Proof.
+NZord_induct p.
+intros n m H; false_hyp H NZlt_irrefl.
+intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_lt in H2. false_hyp H1 H2.
+intros p H IH n m H1. apply -> NZlt_le_succ in H.
+le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n).
+intros n1 m1 H2. apply (NZplus_le_lt_mono_opp n1 m1).
+now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH.
+split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
+apply <- NZle_nlt in H3. le_elim H3.
+apply NZlt_asymm in H2. apply H2. now apply LR.
+rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
+rewrite (NZtimes_lt_pred p (S p)); [reflexivity |].
+rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
+Qed.
+
+Theorem NZtimes_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p).
+Proof.
+intros p n m.
+rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p). now apply NZtimes_lt_mono_neg_l.
+Qed.
+
+Theorem NZtimes_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
+Proof.
+intros n m p H1 H2. le_elim H1.
+le_elim H2. le_less. now apply -> NZtimes_lt_mono_pos_l.
+le_equal; now rewrite H2.
+le_equal; rewrite <- H1; now do 2 rewrite NZtimes_0_l.
+Qed.
+
+Theorem NZtimes_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
+Proof.
+intros n m p H1 H2. le_elim H1.
+le_elim H2. le_less. now apply -> NZtimes_lt_mono_neg_l.
+le_equal; now rewrite H2.
+le_equal; rewrite H1; now do 2 rewrite NZtimes_0_l.
+Qed.
+
+Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
+Proof.
+intros n m p H1 H2; rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
+now apply NZtimes_le_mono_nonneg_l.
+Qed.
+
+Theorem NZtimes_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p.
+Proof.
+intros n m p H1 H2; rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
+now apply NZtimes_le_mono_nonpos_l.
+Qed.
+
+Theorem NZtimes_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof.
+intros n m p H; split; intro H1.
+destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]].
+apply -> NZE_dne; intro H3. apply -> NZneq_lt_or_gt in H3. destruct H3 as [H3 | H3].
+assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_neg_l |].
+rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
+rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+false_hyp H2 H.
+apply -> NZE_dne; intro H3. apply -> NZneq_lt_or_gt in H3. destruct H3 as [H3 | H3].
+assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
+rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
+rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+now rewrite H1.
+Qed.
+
+Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof.
+intros n m p H; do 2 rewrite NZle_lt_or_eq.
+rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
+now rewrite -> (NZtimes_cancel_l n m p);
+[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+Qed.
+
+Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof.
+intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
+apply NZtimes_le_mono_pos_l.
+Qed.
+
+Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
+Proof.
+intros n m p H; do 2 rewrite NZle_lt_or_eq.
+rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
+rewrite -> (NZtimes_cancel_l m n p);
+[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
+Qed.
+
+Theorem NZtimes_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p).
+Proof.
+intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
+apply NZtimes_le_mono_neg_l.
+Qed.
+
+Theorem NZtimes_lt_mono :
+  forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
+Proof.
+intros n m p q H1 H2 H3 H4.
+apply NZle_lt_trans with (m * p).
+apply NZtimes_le_mono_nonneg_r; [assumption | now le_less].
+apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
+Qed.
+
+(* There are still many variants of the theorem above. One can assume 0 < n
+or 0 < p or n <= m or p <= q. *)
+
+Theorem NZtimes_le_mono :
+  forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
+Proof.
+intros n m p q H1 H2 H3 H4.
+le_elim H2; le_elim H4.
+le_less; now apply NZtimes_lt_mono.
+rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now le_less].
+rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now le_less].
+rewrite H2; rewrite H4; now le_equal.
+Qed.
+
+Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_pos_r.
+Qed.
+
+Theorem NZtimes_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n * m.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonneg_r.
+Qed.
+
+Theorem NZtimes_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
+Qed.
+
+Theorem NZtimes_nonpos_nonpos : forall n m : NZ, n <= 0 -> m <= 0 -> 0 <= n * m.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r.
+Qed.
+
+Theorem NZtimes_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
+Qed.
+
+Theorem NZtimes_nonneg_nonpos : forall n m : NZ, 0 <= n -> m <= 0 -> n * m <= 0.
+Proof.
+intros n m H1 H2.
+rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r.
+Qed.
+
+Theorem NZtimes_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
+Proof.
+intros; rewrite NZtimes_comm; now apply NZtimes_pos_neg.
+Qed.
+
+Theorem NZtimes_nonpos_nonneg : forall n m : NZ, n <= 0 -> 0 <= m -> n * m <= 0.
+Proof.
+intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos.
+Qed.
+
+Theorem NZtimes_eq_0 : forall n m : NZ, n * m == 0 -> n == 0 \/ m == 0.
+Proof.
+intros n m H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
+destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
+try (now right); try (now left).
+elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_neg_neg |].
+elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |].
+elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |].
+elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |].
+Qed.
+
+Theorem NZtimes_neq_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof.
+intros n m; split; intro H.
+intro H1; apply NZtimes_eq_0 in H1. tauto.
+split; intro H1; rewrite H1 in H;
+(rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H.
+Qed.
+
+End NZTimesOrderPropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
new file mode 100644
index 000000000..b8940027c
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -0,0 +1,214 @@
+Require Export NAxioms.
+Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
+
+Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
+Open Local Scope NatScope.
+
+(* We call the last property functor on NZ, which includes all the previous
+ones, to get all properties of NZ at once. This way we will include them
+only one time. *)
+
+Module NZOrdAxiomsMod := NNZFunct NAxiomsMod.
+Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
+
+(* Here we probably need to re-prove all axioms declared in NAxioms.v to
+make sure that the definitions like N, S and plus are unfolded in them,
+since unfolding is done only inside a functor. In fact, we'll do it in the
+files that prove the corresponding properties. In those files, we will also
+rename properties proved in NZ files by removing NZ from their names. In
+this way, one only has to consult, for example, NPlus.v to see all
+available properties for plus (i.e., one does not have to go to NAxioms.v
+and NZPlus.v). *)
+
+Theorem E_equiv : equiv N E.
+Proof E_equiv.
+
+Theorem induction :
+  forall A : N -> Prop, predicate_wd E A ->
+    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
+Proof induction.
+
+Theorem pred_0 : P 0 == 0.
+Proof pred_0.
+
+Theorem pred_succ : forall n : N, P (S n) == n.
+Proof pred_succ.
+
+Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
+Proof NZneq_symm.
+
+Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2.
+Proof NZsucc_inj.
+
+Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2.
+Proof NZsucc_inj_wd.
+
+Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
+Proof NZsucc_inj_wd_neg.
+
+(* The theorems NZinduction, NZcentral_induction and the tactic NZinduct
+refer to bidirectional induction, which is not so useful on natural
+numbers. Therefore, we define a new induction tactic for natural numbers.
+We do not have to call "Declare Left Step" and "Declare Right Step"
+commands again, since the data for stepl and stepr tactics is inherited
+from NZ. *)
+
+Tactic Notation "induct" ident(n) := induction_maker n ltac:(apply induction).
+(* FIXME: "Ltac induct n := induction_maker n ltac:(apply induction)" does not work (bug 1703) *)
+
+(* Now we add properties peculiar to natural numbers *)
+
+Theorem nondep_induction :
+  forall A : N -> Prop, predicate_wd E A ->
+    A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
+Proof.
+intros; apply induction; auto.
+Qed.
+
+Tactic Notation "nondep_induct" ident(n) :=
+  induction_maker n ltac:(apply nondep_induction).
+
+(* The fact "forall n : N, S n ~= 0" can be proved either by building a
+function (using recursion) that maps 0 ans S n to two provably different
+terms, or from the axioms of order *)
+
+Theorem neq_succ_0 : forall n : N, S n ~= 0.
+Proof.
+intros n H. apply nlt_0_r with n. rewrite <- H.
+apply <- lt_succ_le. apply <- le_lt_or_eq. now right.
+Qed.
+
+Theorem neq_0 : ~ forall n, n == 0.
+Proof.
+intro H; apply (neq_succ_0 0). apply H.
+Qed.
+
+Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m.
+Proof.
+nondep_induct n. split; intro H;
+[now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].
+intro n; split; intro H; [now exists n | apply neq_succ_0].
+Qed.
+
+Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.
+Proof.
+nondep_induct n; [now left | intros n; right; now exists n].
+Qed.
+
+Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1.
+Proof.
+nondep_induct n.
+rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
+split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
+intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0.
+rewrite succ_inj_wd. tauto.
+Qed.
+
+Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n.
+Proof.
+nondep_induct n.
+intro H; elimtype False; now apply H.
+intros; now rewrite pred_succ.
+Qed.
+
+Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
+Proof.
+intros n m; nondep_induct n.
+intros H; elimtype False; now apply H.
+intros n H1; nondep_induct m.
+intros H; elimtype False; now apply H.
+intros m H2 H3. do 2 rewrite pred_succ in H3. now apply succ_wd.
+Qed.
+
+(* The following induction principle is useful for reasoning about, e.g.,
+Fibonacci numbers *)
+
+Section PairInduction.
+
+Variable A : N -> Prop.
+Hypothesis A_wd : predicate_wd E A.
+
+Add Morphism A with signature E ==> iff as A_morph.
+Proof.
+exact A_wd.
+Qed.
+
+Theorem pair_induction :
+  A 0 -> A 1 ->
+    (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.
+Proof.
+intros until 3.
+assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].
+induct n; [ | intros n [IH1 IH2]]; auto.
+Qed.
+
+End PairInduction.
+
+Tactic Notation "pair_induct" ident(n) := induction_maker n ltac:(apply pair_induction).
+
+(* The following is useful for reasoning about, e.g., Ackermann function *)
+Section TwoDimensionalInduction.
+
+Variable R : N -> N -> Prop.
+Hypothesis R_wd : rel_wd E E R.
+
+Add Morphism R with signature E ==> E ==> iff as R_morph.
+Proof.
+exact R_wd.
+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.
+
+Tactic Notation "two_dim_induct" ident(n) ident(m) :=
+  try intros until n;
+  try intros until m;
+  pattern n, m; apply two_dim_induction; clear n m;
+  [solve_rel_wd | | | ].
+
+Section DoubleInduction.
+
+Variable R : N -> N -> Prop.
+Hypothesis R_wd : rel_wd E E R.
+
+Add Morphism R with signature E ==> E ==> iff as R_morph1.
+Proof.
+exact R_wd.
+Qed.
+
+Theorem double_induction :
+   (forall m : N, R 0 m) ->
+   (forall n : N, R (S n) 0) ->
+   (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m.
+Proof.
+intros H1 H2 H3; induct n; auto.
+intros n IH; nondep_induct m; auto.
+Qed.
+
+End DoubleInduction.
+
+Tactic Notation "double_induct" ident(n) ident(m) :=
+  try intros until n;
+  try intros until m;
+  pattern n, m; apply double_induction; clear n m;
+  [solve_rel_wd | | | ].
+
+End NBasePropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Abstract/NDepRec.v
index 9ad0b4650..9ad0b4650 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Abstract/NDepRec.v
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Abstract/NDomain.v
index a95c94ca0..a95c94ca0 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Abstract/NDomain.v
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 9ee79022e..9ee79022e 100644
--- a/theories/Numbers/Natural/Axioms/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
new file mode 100644
index 000000000..0af5c22fd
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -0,0 +1,164 @@
+Require Export NTimesOrder.
+
+Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Theorem minus_0_r : forall n : N, n - 0 == n.
+Proof minus_0_r.
+
+Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m).
+Proof minus_succ_r.
+
+Theorem minus_1_r : forall n : N, n - 1 == P n.
+Proof.
+intro n; rewrite minus_succ_r; now rewrite minus_0_r.
+Qed.
+
+Theorem minus_0_l : forall n : N, 0 - n == 0.
+Proof.
+induct n.
+apply minus_0_r.
+intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0.
+Qed.
+
+Theorem minus_succ : forall n m : N, S n - S m == n - m.
+Proof.
+intro n; induct m.
+rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ.
+intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r.
+Qed.
+
+Theorem minus_diag : forall n : N, n - n == 0.
+Proof.
+induct n. apply minus_0_r. intros n IH; rewrite minus_succ; now rewrite IH.
+Qed.
+
+Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0.
+Proof.
+intros n m H; elim H using lt_ind_rel; clear n m H.
+solve_rel_wd.
+intro; rewrite minus_0_r; apply neq_succ_0.
+intros; now rewrite minus_succ.
+Qed.
+
+Theorem plus_minus_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p.
+Proof.
+intros n m p; induct p.
+intro; now do 2 rewrite minus_0_r.
+intros p IH H. do 2 rewrite minus_succ_r.
+rewrite <- IH; [now apply le_succ_le |].
+rewrite plus_pred_r. apply minus_gt. now apply <- lt_le_succ.
+reflexivity.
+Qed.
+
+Theorem minus_succ_l : forall n m : N, n <= m -> S m - n == S (m - n).
+Proof.
+intros n m H. rewrite <- (plus_1_l m). rewrite <- (plus_1_l (m - n)).
+symmetry; now apply plus_minus_assoc.
+Qed.
+
+Theorem plus_minus : forall n m : N, (n + m) - m == n.
+Proof.
+intros n m. rewrite <- plus_minus_assoc. apply le_refl.
+rewrite minus_diag; now rewrite plus_0_r.
+Qed.
+
+Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
+Proof.
+intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
+rewrite plus_comm. apply plus_minus.
+Qed.
+
+Theorem plus_minus_eq : forall n m p : N, m + p == n -> n - m == p.
+Proof.
+intros n m p H. symmetry.
+assert (H1 : m + p - m == n - m). now rewrite H.
+rewrite plus_comm in H1. now rewrite plus_minus in H1.
+Qed.
+
+(* This could be proved by adding m to both sides. Then the proof would
+use plus_minus_assoc and le_minus_0, which is proven below. *)
+Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
+Proof.
+intros n m p H; double_induct n m.
+intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H.
+intro n; rewrite minus_0_r; now rewrite plus_0_l.
+intros n m IH H1. rewrite minus_succ in H1. apply IH in H1.
+rewrite plus_succ_l; now apply succ_wd.
+Qed.
+
+Theorem minus_plus_distr : forall n m p : N, n - (m + p) == (n - m) - p.
+Proof.
+intros n m; induct p.
+rewrite plus_0_r; now rewrite minus_0_r.
+intros p IH. rewrite plus_succ_r; do 2 rewrite minus_succ_r. now rewrite IH.
+Qed.
+
+Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
+Proof.
+intros n m p H.
+rewrite (plus_comm n m).
+rewrite <- plus_minus_assoc; [assumption |].
+now rewrite (plus_comm m (n - p)).
+Qed.
+
+(** Minus and order *)
+
+Theorem le_minus_l : forall n m : N, n - m <= n.
+Proof.
+intro n; induct m.
+rewrite minus_0_r; le_equal.
+intros m IH. rewrite minus_succ_r.
+apply le_trans with (n - m); [apply le_pred_l | assumption].
+Qed.
+
+Theorem le_minus_0 : forall n m : N, n <= m <-> n - m == 0.
+Proof.
+double_induct n m.
+intro m; split; intro; [apply minus_0_l | apply le_0_l].
+intro m; rewrite minus_0_r; split; intro H;
+[false_hyp H nle_succ_0 | false_hyp H neq_succ_0].
+intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ.
+Qed.
+
+(** Minus and times *)
+
+Theorem times_pred_r : forall n m : N, n * (P m) == n * m - n.
+Proof.
+intro n; nondep_induct m.
+now rewrite pred_0, times_0_r, minus_0_l.
+intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
+le_equal.
+now rewrite minus_diag, plus_0_r.
+Qed.
+
+Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
+Proof.
+intros n m p; induct n.
+now rewrite minus_0_l, times_0_l, minus_0_l.
+intros n IH. destruct (le_lt_dec m n) as [H | H].
+rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
+rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
+rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
+now apply <- plus_cancel_l.
+assert (H1 : S n <= m); [now apply -> lt_le_succ |].
+setoid_replace (S n - m) with 0 by now apply -> le_minus_0.
+setoid_replace ((S n * p) - m * p) with 0 by (apply -> le_minus_0; now apply times_le_mono_r).
+apply times_0_l.
+Qed.
+
+Theorem times_minus_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
+Proof.
+intros n m p; rewrite (times_comm p (n - m)), (times_comm p n), (times_comm p m).
+apply times_minus_distr_r.
+Qed.
+
+End NMinusPropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v
index 82a922453..82a922453 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v
diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index b4f363901..773f5d97e 100644
--- a/theories/Numbers/Natural/Axioms/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -1,76 +1,26 @@
-Require Export NBase.
-Require Import NZOrder.
+Require Export NTimes.
 
-Module Type NOrderSig.
-Declare Module Export NBaseMod : NBaseSig.
+Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Parameter Inline lt : N -> N -> Prop.
-Parameter Inline le : N -> N -> Prop.
+(* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
 
-Notation "x < y" := (lt x y) : NatScope.
-Notation "x <= y" := (le x y) : NatScope.
-Notation "x > y" := (lt y x) (only parsing) : NatScope.
-Notation "x >= y" := (le y x) (only parsing) : NatScope.
+(* Axioms *)
 
-Add Morphism lt with signature E ==> E ==> iff as lt_wd.
-Add Morphism le with signature E ==> E ==> iff as le_wd.
+Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
+Proof le_lt_or_eq.
 
-Axiom le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
-Axiom nlt_0_r : forall x, ~ (x < 0).
-Axiom lt_succ_le : forall x y, x < S y <-> x <= y.
+Theorem nlt_0_r : forall x, ~ (x < 0).
+Proof nlt_0_r.
 
-End NOrderSig.
+Theorem lt_succ_le : forall x y, x < S y <-> x <= y.
+Proof lt_succ_le.
 
-Module NOrderPropFunct (Import NOrderModule : NOrderSig).
-Module Export NBasePropMod := NBasePropFunct NBaseMod.
-Open Local Scope NatScope.
-
-Ltac le_intro1 := rewrite le_lt_or_eq; left.
-Ltac le_intro2 := rewrite le_lt_or_eq; right.
-Ltac le_elim H := rewrite le_lt_or_eq in H; destruct H as [H | H].
-
-Theorem lt_succ_lt : forall n m : N, S n < m -> n < m.
-Proof.
-intro n; induct m.
-intro H; false_hyp H nlt_0_r.
-intros m IH H. apply <- lt_succ_le. apply -> lt_succ_le in H. le_elim H.
-le_intro1; now apply IH.
-rewrite <- H; le_intro1. apply <- lt_succ_le; now le_intro2.
-Qed.
+(* Renaming theorems from NZOrder.v *)
 
 Theorem lt_irrefl : forall n : N, ~ (n < n).
-Proof.
-induct n.
-apply nlt_0_r.
-intros n IH H. apply -> lt_succ_le in H; le_elim H.
-apply lt_succ_lt in H; now apply IH.
-assert (n < S n) by (apply <- lt_succ_le; now le_intro2).
-rewrite H in *; now apply IH.
-Qed.
-
-Module NZOrderMod <: NZOrderSig.
-Module NZBaseMod := NZBaseMod.
-
-Definition NZlt := lt.
-Definition NZle := le.
-
-Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
-Proof lt_wd.
-
-Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
-Proof le_wd.
-
-Definition NZle_lt_or_eq := le_lt_or_eq.
-Definition NZlt_succ_le := lt_succ_le.
-Definition NZlt_succ_lt := lt_succ_lt.
-Definition NZlt_irrefl := lt_irrefl.
-
-End NZOrderMod.
-
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
-
-(* Renaming theorems from NZOrder.v *)
+Proof NZOrdAxiomsMod.NZlt_irrefl.
 
 Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
 Proof NZlt_le_incl.
@@ -108,6 +58,9 @@ Proof NZnle_succ_l.
 Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m.
 Proof NZlt_le_succ.
 
+Theorem lt_succ_lt : forall n m : N, S n < m -> n < m.
+Proof NZlt_succ_lt.
+
 Theorem le_succ_le : forall n m : N, S n <= m -> n <= m.
 Proof NZle_succ_le.
 
@@ -196,13 +149,13 @@ Theorem left_induction :
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
-Theorem central_induction :
+Theorem order_induction :
   forall A : N -> Prop, predicate_wd E A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n < z  -> A (S n) -> A n) ->
         forall n : N, A n.
-Proof NZcentral_induction.
+Proof NZorder_induction.
 
 Theorem right_induction' :
   forall A : N -> Prop, predicate_wd E A ->
@@ -245,7 +198,7 @@ Proof NZle_ind.
 Theorem le_0_l : forall n : N, 0 <= n.
 Proof.
 induct n.
-now le_intro2.
+now le_equal.
 intros; now apply le_le_succ.
 Qed.
 
@@ -254,9 +207,11 @@ Proof.
 intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r.
 Qed.
 
-Theorem le_0_eq_0 : forall n, n <= 0 -> n == 0.
+Theorem le_0_eq_0 : forall n, n <= 0 <-> n == 0.
 Proof.
-intros n H; le_elim H; [false_hyp H nlt_0_r | assumption].
+intros n; split; intro H.
+le_elim H; [false_hyp H nlt_0_r | assumption].
+le_equal.
 Qed.
 
 Theorem lt_0_succ : forall n, 0 < S n.
@@ -271,9 +226,11 @@ trivial.
 intros n IH H. apply IH; now apply lt_succ_lt.
 Qed.
 
-Theorem neq_0_lt_0 : forall n, 0 ~= n -> 0 < n.
+Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
 Proof.
-nondep_induct n. intro H; now elim H. intros; apply lt_0_succ.
+nondep_induct n.
+split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
+intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
 Qed.
 
 Lemma Acc_nonneg_lt : forall n : N,
@@ -309,7 +266,7 @@ intros Base Step; induct n.
 intros; apply Base.
 intros n IH m H. elim H using le_ind.
 solve_predicate_wd.
-apply Step; [| apply IH]; now le_intro2.
+apply Step; [| apply IH]; now le_equal.
 intros k H1 H2. apply le_succ_le in H1. auto.
 Qed.
 
@@ -329,6 +286,103 @@ Qed.
 
 End RelElim.
 
+(** Predecessor and order *)
+
+Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n.
+Proof.
+intros n H; apply succ_pred; intro H1; rewrite H1 in H.
+false_hyp H lt_irrefl.
+Qed.
+
+Theorem le_pred_l : forall n : N, P n <= n.
+Proof.
+nondep_induct n.
+rewrite pred_0; le_equal.
+intros; rewrite pred_succ;  apply le_succ_r.
+Qed.
+
+Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
+Proof.
+nondep_induct n.
+intro H; elimtype False; now apply H.
+intros; rewrite pred_succ;  apply lt_succ_r.
+Qed.
+
+Theorem le_le_pred : forall n m : N, n <= m -> P n <= m.
+Proof.
+intros n m H; apply le_trans with n. apply le_pred_l. assumption.
+Qed.
+
+Theorem lt_lt_pred : forall n m : N, n < m -> P n < m.
+Proof.
+intros n m H; apply le_lt_trans with n. apply le_pred_l. assumption.
+Qed.
+
+Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *)
+Proof.
+intro n; nondep_induct m.
+intro H; false_hyp H nlt_0_r.
+intros m IH. rewrite pred_succ; now apply -> lt_succ_le.
+Qed.
+
+Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
+Proof.
+intros n m; nondep_induct n.
+rewrite pred_0; intro H; le_less.
+intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ.
+Qed.
+
+Theorem lt_pred_lt : forall n m : N, n < P m -> n < m.
+Proof.
+intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l].
+Qed.
+
+Theorem le_pred_le : forall n m : N, n <= P m -> n <= m.
+Proof.
+intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l].
+Qed.
+
+Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *)
+Proof.
+intros n m H; elim H using le_ind_rel.
+solve_rel_wd.
+intro; rewrite pred_0; apply le_0_l.
+intros p q H1 _; now do 2 rewrite pred_succ.
+Qed.
+
+Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
+Proof.
+intros n m H1; split; intro H2.
+assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
+now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
+[apply <- succ_lt_mono | | |].
+assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
+apply lt_le_trans with (P m). assumption. apply le_pred_l.
+apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2.
+Qed.
+
+Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
+Proof.
+intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
+Qed.
+
+Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
+Proof.
+intros n m H. apply lt_le_pred. now apply <- lt_le_succ.
+Qed.
+
+Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *)
+Proof.
+intros n m H. apply <- lt_succ_le. now apply lt_pred_le.
+Qed.
+
+Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
+Proof.
+intros n m; nondep_induct n.
+rewrite pred_0. split; intro H; apply le_0_l.
+intro n. rewrite pred_succ. apply succ_le_mono.
+Qed.
+
 End NOrderPropFunct.
 
 
diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Abstract/NOtherInd.v
index 9b01e5143..9b01e5143 100644
--- a/theories/Numbers/Natural/Axioms/NOtherInd.v
+++ b/theories/Numbers/Natural/Abstract/NOtherInd.v
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 5f5a88bca..67a2766ba 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -1,50 +1,14 @@
-Require Import NZPlus.
 Require Export NBase.
 
-Module Type NPlusSig.
-
-Declare Module Export NBaseMod : NBaseSig.
+Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Parameter Inline plus : N -> N -> N.
-
-Notation "x + y" := (plus x y) : NatScope.
-
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
-
-Axiom plus_0_l : forall n : N, 0 + n == n.
-Axiom plus_succ_l : forall n m : N, (S n) + m == S (n + m).
-
-End NPlusSig.
-
-Module NPlusPropFunct (Import NPlusMod : NPlusSig).
-Module Export NBasePropMod := NBasePropFunct NBaseMod.
-Open Local Scope NatScope.
-
-(*Theorem plus_wd : fun2_wd E E E plus.
-Proof plus_wd.
-
 Theorem plus_0_l : forall n : N, 0 + n == n.
 Proof plus_0_l.
 
 Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m).
-Proof plus_succ_l.*)
-
-Module NZPlusMod <: NZPlusSig.
-
-Module NZBaseMod <: NZBaseSig := NZBaseMod.
-
-Definition NZplus := plus.
-
-(* Axioms*)
-Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd.
-Proof plus_wd.
-Definition NZplus_0_l := plus_0_l.
-Definition NZplus_succ_l := plus_succ_l.
-
-End NZPlusMod.
-
-Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
+Proof plus_succ_l.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -86,8 +50,8 @@ intros n m; induct n.
 (* The next command does not work with the axiom plus_0_l from NPlusSig *)
 rewrite plus_0_l. intuition reflexivity.
 intros n IH. rewrite plus_succ_l.
-rewrite_false (S (n + m) == 0) succ_neq_0.
-rewrite_false (S n == 0) succ_neq_0. tauto.
+rewrite_false (S (n + m) == 0) neq_succ_0.
+rewrite_false (S n == 0) neq_succ_0. tauto.
 Qed.
 
 Theorem plus_eq_succ :
@@ -98,7 +62,7 @@ intros n m; nondep_induct n.
 split; intro H.
 destruct H as [p H]. rewrite plus_0_l in H; right; now exists p.
 destruct H as [[n' H] | [m' H]].
-symmetry in H; false_hyp H succ_neq_0.
+symmetry in H; false_hyp H neq_succ_0.
 exists m'; now rewrite plus_0_l.
 intro n; split; intro H.
 left; now exists n.
@@ -120,11 +84,24 @@ Qed.
 Theorem succ_plus_discr : forall n m : N, m ~= S (n + m).
 Proof.
 intro n; induct m.
-apply neq_symm. apply succ_neq_0.
+apply neq_symm. apply neq_succ_0.
 intros m IH H. apply succ_inj in H. rewrite plus_succ_r in H.
 unfold not in IH; now apply IH.
 Qed.
 
+Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
+Proof.
+intros n m; nondep_induct n.
+intro H; now elim H.
+intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ.
+Qed.
+
+Theorem plus_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
+Proof.
+intros n m H; rewrite (plus_comm n (P m));
+rewrite (plus_comm n m); now apply plus_pred_l.
+Qed.
+
 (* One could define n <= m as exists p : N, p + n == m. Then we have
 dichotomy:
 
diff --git a/theories/Numbers/Natural/Axioms/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index c3e8cb663..df4c94614 100644
--- a/theories/Numbers/Natural/Axioms/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -4,7 +4,7 @@ Require Import NZPlusOrder.
 
 Module NPlusOrderPropFunct
   (Import NPlusMod : NPlusSig)
-  (Import NOrderMod : NOrderSig with Module NBaseMod := NPlusMod.NBaseMod).
+  (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod).
 Module Export NPlusPropMod := NPlusPropFunct NPlusMod.
 Module Export NOrderPropMod := NOrderPropFunct NOrderMod.
 Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod.
diff --git a/theories/Numbers/Natural/Axioms/NPred.v b/theories/Numbers/Natural/Abstract/NPred.v
index 711d6b883..711d6b883 100644
--- a/theories/Numbers/Natural/Axioms/NPred.v
+++ b/theories/Numbers/Natural/Abstract/NPred.v
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index c35a6693b..c35a6693b 100644
--- a/theories/Numbers/Natural/Axioms/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 94bd8d26e..7d42a812c 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -2,63 +2,16 @@ Require Export Ring.
 (* Since we define a ring below, it should be possible to call the tactic
 ring in the modules that use this module. Hence Export, not Import. *)
 Require Export NPlus.
-Require Import NZTimes.
 
-Module Type NTimesSig.
-Declare Module Export NPlusMod : NPlusSig.
+Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Parameter Inline times : N -> N -> N.
-
-Notation "x * y" := (times x y) : NatScope.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
-
-Axiom times_0_r : forall n, n * 0 == 0.
-Axiom times_succ_r : 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 A * B 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 NTimesSig.
-
-Module NTimesPropFunct (Import NTimesMod : NTimesSig).
-Module Export NPlusPropMod := NPlusPropFunct NPlusMod.
-Open Local Scope NatScope.
-
-(*Theorem times_wd : fun2_wd E E E times.
-Proof times_wd.
-
 Theorem times_0_r : forall n, n * 0 == 0.
 Proof times_0_r.
 
 Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
-Proof times_succ_r.*)
-
-Module NZTimesMod <: NZTimesSig.
-Module NZPlusMod <: NZPlusSig := NZPlusMod.
-Definition NZtimes := times.
-
-(* Axioms *)
-
-Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd.
-Proof times_wd.
-Definition NZtimes_0_r := times_0_r.
-Definition NZtimes_succ_r := times_succ_r.
-
-End NZTimesMod.
-
-Module Export NZTimesPropMod := NZTimesPropFunct NZTimesMod.
+Proof times_succ_r.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -110,19 +63,19 @@ intros; now left.
 intros; now left.
 intros; now right.
 intros m IH H1. rewrite times_succ_l in H1.
-rewrite plus_succ_r in H1. now apply succ_neq_0 in H1.
+rewrite plus_succ_r in H1. now apply neq_succ_0 in H1.
 Qed.
 
 Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1.
 Proof.
 intros n m; induct n.
-intro H; rewrite times_0_l in H; symmetry in H; false_hyp H succ_neq_0.
+intro H; rewrite times_0_l in H; symmetry in H; false_hyp H neq_succ_0.
 intros n IH H. rewrite times_succ_l in H. apply plus_eq_1 in H.
 destruct H as [[H1 H2] | [H1 H2]].
-apply IH in H1. destruct H1 as [_ H1]. rewrite H1 in H2; false_hyp H2 succ_neq_0.
+apply IH in H1. destruct H1 as [_ H1]. rewrite H1 in H2; false_hyp H2 neq_succ_0.
 apply times_eq_0 in H1. destruct H1 as [H1 | H1].
 rewrite H1; now split.
-rewrite H2 in H1; false_hyp H1 succ_neq_0.
+rewrite H2 in H1; false_hyp H1 neq_succ_0.
 Qed.
 
 (* In proving the correctness of the definition of multiplication on
@@ -144,7 +97,7 @@ Theorem plus_times_repl_pair : forall a n m n' m' u v,
   a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
 intros a n m n' m' u v H1 H2.
-apply (times_wd a a) in H2; [| reflexivity].
+apply (@times_wd a a) in H2; [| reflexivity].
 do 2 rewrite times_plus_distr_l in H2.
 symmetry in H2; add_equations H1 H2 as H3.
 stepl (a * n + (u + a * n' + a * m)) in H3 by ring.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
new file mode 100644
index 000000000..19b9e0ae4
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -0,0 +1,133 @@
+Require Export NOrder.
+
+Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
+Proof NZplus_lt_mono_l.
+
+Theorem plus_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.
+Proof NZplus_lt_mono_r.
+
+Theorem plus_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.
+Proof NZplus_lt_mono.
+
+Theorem plus_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.
+Proof NZplus_le_mono_l.
+
+Theorem plus_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.
+Proof NZplus_le_mono_r.
+
+Theorem plus_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.
+Proof NZplus_le_mono.
+
+Theorem plus_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.
+Proof NZplus_lt_le_mono.
+
+Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
+Proof NZplus_le_lt_mono.
+
+Theorem plus_le_lt_mono_opp : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
+Proof NZplus_le_lt_mono_opp.
+
+Theorem plus_lt_inv : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
+Proof NZplus_lt_inv.
+
+Theorem plus_gt_inv_0 : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
+Proof NZplus_gt_inv_0.
+
+(** Theorems true for natural numbers *)
+
+Theorem le_plus_r : forall n m : N, n <= n + m.
+Proof.
+intro n; induct m.
+rewrite plus_0_r; le_equal.
+intros m IH. rewrite plus_succ_r; now apply le_le_succ.
+Qed.
+
+Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
+Proof.
+intro n; nondep_induct m.
+intro H; elimtype False; now apply H.
+intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
+Qed.
+
+Theorem lt_lt_plus : forall n m p : N, n < m -> n < m + p.
+Proof.
+intros n m p H; rewrite <- (plus_0_r n).
+apply plus_lt_le_mono; [assumption | apply le_0_l].
+Qed.
+
+(* The following property is similar to plus_repl_pair in NPlus.v
+and is used to prove the correctness of the definition of order
+on integers constructed from pairs of natural numbers *)
+
+Theorem plus_lt_repl_pair : forall n m n' m' u v,
+  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
+Proof.
+intros n m n' m' u v H1 H2.
+symmetry in H2. assert (H3 : n' + m <= n + m'); [now le_equal |].
+assert (H4 : n + u + (n' + m) < m + v + (n + m')); [now apply plus_lt_le_mono |].
+stepl (n + (m + (n' + u))) in H4 by ring. stepr (n + (m + (m' + v))) in H4 by ring.
+now do 2 apply <- plus_lt_mono_l in H4.
+Qed.
+
+(** Multiplication and order *)
+
+Theorem times_lt_pred :
+  forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Proof NZtimes_lt_pred.
+
+Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZtimes_lt_mono_pos_l.
+
+Theorem times_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZtimes_lt_mono_pos_r.
+
+Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
+Proof.
+intros; apply NZtimes_le_mono_nonneg_l. apply le_0_l. assumption.
+Qed.
+
+Theorem times_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p.
+Proof.
+intros; apply NZtimes_le_mono_nonneg_r. apply le_0_l. assumption.
+Qed.
+
+Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZtimes_cancel_l.
+
+Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZtimes_le_mono_pos_l.
+
+Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZtimes_le_mono_pos_r.
+
+Theorem times_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
+Proof.
+intros; apply NZtimes_lt_mono; try assumption; apply le_0_l.
+Qed.
+
+Theorem times_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q.
+Proof.
+intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
+Qed.
+
+Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZtimes_pos_pos.
+
+Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0.
+Proof NZtimes_eq_0.
+
+Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZtimes_neq_0.
+
+End NTimesOrderPropFunct.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Axioms/NBase.v b/theories/Numbers/Natural/Axioms/NBase.v
deleted file mode 100644
index fd483265d..000000000
--- a/theories/Numbers/Natural/Axioms/NBase.v
+++ /dev/null
@@ -1,196 +0,0 @@
-Require Export NumPrelude.
-Require Import NZBase.
-
-Module Type NBaseSig.
-
-Parameter Inline N : Set.
-Parameter Inline E : N -> N -> Prop.
-Parameter Inline O : N.
-Parameter Inline S : N -> N.
-
-Delimit Scope NatScope with Nat.
-Open Local Scope NatScope.
-
-Notation "x == y" := (E x y) (at level 70) : NatScope.
-Notation "x ~= y" := (~ E x y) (at level 70) : NatScope.
-Notation "0" := O : NatScope.
-Notation "1" := (S O) : NatScope.
-
-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.
-
-Add Morphism S with signature E ==> E as S_wd.
-
-Axiom succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2.
-Axiom succ_neq_0 : forall n : N, S n ~= 0.
-
-Axiom induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
-
-End NBaseSig.
-
-Module NBasePropFunct (Import NBaseMod : NBaseSig).
-Open Local Scope NatScope.
-
-(*Theorem E_equiv : equiv N E.
-Proof E_equiv.
-
-Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2.
-Proof succ_inj_wd.
-
-Theorem succ_neq_0 : forall n : N, S n ~= 0.
-Proof succ_neq_0.
-
-Theorem induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
-Proof induction.*)
-
-Module NZBaseMod <: NZBaseSig.
-Definition NZ := N.
-Definition NZE := E.
-Definition NZ0 := 0.
-Definition NZsucc := S.
-
-(* Axioms *)
-Definition NZE_equiv := E_equiv.
-Definition NZsucc_inj := succ_inj.
-
-Add Relation NZ NZE
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
-
-Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
-Proof S_wd.
-
-Theorem NZinduction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A n <-> A (S n)) -> forall n : N, A n.
-Proof.
-intros A A_wd Base Step.
-apply induction; try assumption.
-intros; now apply -> Step.
-Qed.
-
-End NZBaseMod.
-
-Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
-
-Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
-Proof NZneq_symm.
-
-Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
-Proof NZsucc_inj_wd_neg.
-
-Ltac induct n := induction_maker n ltac:(apply induction).
-
-Theorem nondep_induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
-Proof.
-intros; apply induction; auto.
-Qed.
-
-Ltac nondep_induct n := induction_maker n ltac:(apply nondep_induction).
-
-Theorem neq_0 : ~ forall n, n == 0.
-Proof.
-intro H; apply (succ_neq_0 0). apply H.
-Qed.
-
-Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m.
-Proof.
-nondep_induct n. split; intro H;
-[now elim H | destruct H as [m H]; symmetry in H; false_hyp H succ_neq_0].
-intro n; split; intro H; [now exists n | apply succ_neq_0].
-Qed.
-
-Theorem zero_or_succ : 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 A : N -> Prop.
-Hypothesis A_wd : predicate_wd E A.
-
-Add Morphism A with signature E ==> iff as A_morph.
-Proof.
-exact A_wd.
-Qed.
-
-Theorem double_induction :
-  A 0 -> A 1 ->
-    (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.
-Proof.
-intros until 3.
-assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].
-induct n; [ | intros n [IH1 IH2]]; auto.
-Qed.
-
-End DoubleInduction.
-
-Ltac double_induct n := induction_maker n ltac:(apply double_induction).
-
-(* The following is useful for reasoning about, e.g., Ackermann function *)
-Section TwoDimensionalInduction.
-
-Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd E E R.
-
-Add Morphism R with signature E ==> E ==> iff as R_morph.
-Proof.
-exact R_wd.
-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.
-
-Ltac two_dim_induct n m :=
-  try intros until n;
-  try intros until m;
-  pattern n, m; apply two_dim_induction; clear n m;
-  [unfold rel_wd; unfold fun2_wd;
-   let x1 := fresh "x" in
-   let y1 := fresh "y" in
-   let H1 := fresh "H" in
-   let x2 := fresh "x" in
-   let y2 := fresh "y" in
-   let H2 := fresh "H" in
-     intros x1 y1 H1 x2 y2 H2;
-     qsetoid_rewrite H1;
-     qiff x2 y2 H2 | | | ].
-(* This is not a very efficient approach because qsetoid_rewrite uses
-qiff to take the formula apart in order to make it quantifier-free,
-and then qiff is called again and takes the formula apart for the
-second time. It is better to analyze the formula once and generalize
-qiff to take a list of equalities that it has to rewrite. *)
-
-End NBasePropFunct.
-
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Axioms/NLeibniz.v b/theories/Numbers/Natural/Axioms/NLeibniz.v
deleted file mode 100644
index d9c4718aa..000000000
--- a/theories/Numbers/Natural/Axioms/NLeibniz.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* This file proves or redefines properties that are true for Leibniz
-equality. For example, it removes the premise predicate_wd from
-induction theorems. *)
-
diff --git a/theories/Numbers/Natural/Axioms/NMinus.v b/theories/Numbers/Natural/Axioms/NMinus.v
deleted file mode 100644
index 2bac3c5c3..000000000
--- a/theories/Numbers/Natural/Axioms/NMinus.v
+++ /dev/null
@@ -1,88 +0,0 @@
-Require Export NPlusOrder.
-
-Module Type NMinusSignature.
-Declare Module Export NPredModule : NPredSignature.
-Open Local Scope NatScope.
-
-Parameter Inline minus : N -> N -> N.
-
-Notation "x - y" := (minus x y) : NatScope.
-
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
-
-Axiom minus_0_r : forall n, n - 0 == n.
-Axiom minus_succ_r : forall n m, n - (S m) == P (n - m).
-
-End NMinusSignature.
-
-Module NMinusProperties (Import NMinusModule : NMinusSignature)
-                        (Import NPlusMod : NPlusSig with
-                          Module NBaseMod := NMinusModule.NPredModule.NBaseMod)
-                        (Import NOrderModule : NOrderSig with
-                          Module NBaseMod := NMinusModule.NPredModule.NBaseMod).
-Module Export NPlusOrderPropertiesModule :=
-  NPlusOrderProperties NPlusMod NOrderModule.
-Open Local Scope NatScope.
-
-Theorem minus_1_r : forall n, n - 1 == P n.
-Proof.
-intro n; rewrite minus_succ_r; now rewrite minus_0_r.
-Qed.
-
-Theorem minus_0_l : forall n, 0 - n == 0.
-Proof.
-induct n.
-apply minus_0_r.
-intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0.
-Qed.
-
-Theorem minus_comm_succ : forall n m, S n - S m == n - m.
-Proof.
-intro n; induct m.
-rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ.
-intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r.
-Qed.
-
-Theorem minus_succ_l : forall n m, n <= m -> S m - n == S (m - n).
-Proof.
-intros n m H; pattern n, m; apply le_ind_rel.
-unfold rel_wd. intros x x' H1 y y' H2; rewrite H1; now rewrite H2.
-intros; now do 2 rewrite minus_0_r.
-clear n m H. intros n m H1 H2.
-now do 2 rewrite minus_comm_succ. assumption.
-Qed.
-
-Theorem minus_le : forall n m, n <= m -> n - m == 0.
-Proof.
-intros n m H; pattern n, m; apply le_ind_rel.
-unfold rel_wd; intros x x' H1 y y' H2; rewrite H1; now rewrite H2.
-apply minus_0_l.
-clear n m H; intros n m H1 H2. now rewrite minus_comm_succ.
-assumption.
-Qed.
-
-Theorem minus_diag : forall n, n - n == 0.
-Proof.
-intro n; apply minus_le; apply le_refl.
-Qed.
-
-Theorem minus_plus : forall n m, n <= m -> (m - n) + n == m.
-Proof.
-intros n m H; pattern n, m; apply le_ind_rel.
-unfold rel_wd; intros x x' H1 y y' H2; rewrite H1; now rewrite H2.
-intro; rewrite minus_0_r; now rewrite plus_0_r.
-clear n m H. intros n m _ H2. rewrite minus_comm_succ. rewrite plus_succ_r.
-now rewrite H2.
-assumption.
-Qed.
-
-End NMinusProperties.
-
-
-
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Axioms/NRec.v b/theories/Numbers/Natural/Axioms/NRec.v
deleted file mode 100644
index d74660c4a..000000000
--- a/theories/Numbers/Natural/Axioms/NRec.v
+++ /dev/null
@@ -1,259 +0,0 @@
-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_succ :
-  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_succ 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_succ :
-  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_succ (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_succ 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_succ [A].
-
-Definition if_zero (A : Set) (a b : A) (n : N) : A :=
-  recursion a (fun _ _ => b) n.
-
-Add Morphism if_zero with signature LE_succet ==> LE_succet ==> E ==> LE_succet as if_zero_wd.
-Proof.
-unfold LE_succet.
-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_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
-Proof.
-intros; unfold if_zero.
-now rewrite (recursion_succ (@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 succ_0 : forall n, ~ S n == 0.
-Proof.
-intros n H.
-assert (true = false); [| discriminate].
-replace true with (if_zero false true (S n)) by apply if_zero_succ.
-pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0.
-change (LE_succet bool (if_zero false true (S n)) (if_zero false true 0)).
-rewrite H. unfold LE_succet. reflexivity.
-Qed.
-
-Theorem succ_inj : forall m n, S m == S n -> m == n.
-Proof.
-intros m n H.
-setoid_replace m with (A (S m)) by (symmetry; apply pred_succ).
-setoid_replace n with (A (S n)) by (symmetry; apply pred_succ).
-now apply pred_wd.
-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 : N, m + n == 1 ->  (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0).
-induct m.
-intros n H; rewrite plus_0_l in H; left; now split.
-intros n IH m H; rewrite plus_succ_l in H; apply succ_inj in H;
-apply plus_eq_0 in H; destruct H as [H1 H2];
-now right; split; [apply succ_wd |].
-Qed.
-
-Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m.
-
-Theorem 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.
-
-Theorem plus_eq_1_dec_0 : forall n : N, plus_eq_1_dec 0 n = true.
-Proof.
-intro n. unfold plus_eq_1_dec.
-now apply recursion_0.
-Qed.
-
-Theorem plus_eq_1_dec_succ : forall m n : N, plus_eq_1_dec (S n) m = false.
-Proof.
-intros n m. unfold plus_eq_1_dec.
-now rewrite (recursion_succ eq_bool);
-[| unfold eq_bool | apply plus_eq_1_dec_step_wd].
-Qed.
-
-Theorem plus_eq_1_dec_correct :
-  forall m n : 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_succ.
-split; [intro H1; discriminate | intros _ ].
-rewrite plus_succ_l in H. apply succ_inj in H.
-apply plus_eq_0 in H; split; [apply succ_wd | ]; tauto.
-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_succ eq_bool);
-[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros].
-intro m; rewrite (recursion_succ eq_bool).
-rewrite times_succ_l. rewrite plus_succ_r. intro H; now apply succ_0 in H.
-now unfold eq_bool.
-unfold fun2_wd; intros; now unfold eq_bool.
-Qed.
diff --git a/theories/Numbers/Natural/Axioms/NTimesOrder.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v
deleted file mode 100644
index 3e7c3f2b2..000000000
--- a/theories/Numbers/Natural/Axioms/NTimesOrder.v
+++ /dev/null
@@ -1,70 +0,0 @@
-Require Export NTimes.
-Require Export NPlusOrder.
-
-Module NTimesOrderProperties (Import NTimesMod : NTimesSig)
-                          (Import NOrderModule : NOrderSig with
-                            Module NBaseMod := NTimesMod.NPlusMod.NBaseMod).
-Module Export NTimesPropertiesModule :=  NTimesPropFunct NTimesMod.
-Module Export NPlusOrderPropertiesModule :=
-  NPlusOrderProperties NTimesMod.NPlusMod NOrderModule.
-Open Local Scope NatScope.
-
-Lemma times_succ_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 times_1_l.
-intros x IH H.
-rewrite times_succ_l.
-set (k := S x * m); rewrite times_succ_l; unfold k; clear k.
-apply plus_lt_compat; [apply IH; assumption | assumption].
-Qed.
-
-Lemma times_succ_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 times_comm; unfold k; clear k.
-set (k := ((S n) * m)); rewrite times_comm; unfold k; clear k.
-now apply times_succ_lt_compat_l.
-Qed.
-
-Lemma times_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 times_succ_lt_compat_l.
-Qed.
-
-Lemma times_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 times_succ_lt_compat_r.
-Qed.
-
-Lemma times_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m.
-Proof.
-intros n m H1 H2.
-rewrite <- (times_0_l m); now apply times_lt_compat_r.
-Qed.
-
-Lemma times_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_l; apply times_positive;
-[assumption | apply lt_positive with (n := p); assumption].
-intros x IH H1 H2.
-apply lt_trans with (m := ((S x) * q)).
-now apply times_succ_lt_compat_l; assumption.
-now apply times_lt_compat_r; [| apply lt_positive with (n := p)].
-Qed.
-
-End NTimesOrderProperties.
-
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 46973db7f..165c1211f 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,30 +1,44 @@
 Require Import NArith.
-Require Import Ndec.
+Require Import NMinus.
 
-Require Export NDepRec.
-Require Export NTimesOrder.
-Require Export NMinus.
-Require Export NMiscFunct.
+Module NBinaryAxiomsMod <: NAxiomsSig.
 
 Open Local Scope N_scope.
 
-Module NBinaryDomain : NDomainEqSignature
-  with Definition N := N
-  with Definition E := (@eq N)
-  with Definition e := Neqb.
-
 Definition N := N.
 Definition E := (@eq N).
-Definition e := Neqb.
+Definition O := 0.
+Definition S := Nsucc.
 
-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 Npred (n : N) := match n with
+| 0 => 0
+| Npos p => match p with
+  | xH => 0
+  | _ => Npos (Ppred p)
+  end
+end.*)
 
-Definition E_equiv : equiv N E := eq_equiv N.
+Definition P := Npred.
+Definition plus := Nplus.
+Definition minus := Nminus.
+
+(*Definition minus (n m : N) :=
+match n, m with
+| N0, _ => N0
+| n, N0 => n
+| Npos n', Npos m' =>
+  match Pminus_mask n' m' with
+  | IsPos p => Npos p
+  | _ => N0
+  end
+end.*)
+
+Definition times := Nmult.
+Definition lt := Nlt.
+Definition le := Nle.
+
+Theorem E_equiv : equiv N E.
+Proof (eq_equiv N).
 
 Add Relation N E
  reflexivity proved by (proj1 E_equiv)
@@ -32,24 +46,102 @@ Add Relation N E
  transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
-End NBinaryDomain.
+Add Morphism S with signature E ==> E as succ_wd.
+Proof.
+congruence.
+Qed.
 
-Module BinaryNat <: NBaseSig.
-Module Export NDomainModule := NBinaryDomain.
+Add Morphism P with signature E ==> E as pred_wd.
+Proof.
+congruence.
+Qed.
 
-Definition O := N0.
-Definition S := Nsucc.
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+congruence.
+Qed.
 
-Add Morphism S with signature E ==> E as succ_wd.
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
 Proof.
 congruence.
 Qed.
 
+Add Morphism lt with signature E ==> E ==> iff as lt_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Add Morphism le with signature E ==> E ==> iff as le_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
 Theorem induction :
-  forall P : N -> Prop, predicate_wd E P ->
-    P 0 -> (forall n, P n -> P (S n)) -> forall n, P n.
+  forall A : N -> Prop, predicate_wd E A ->
+    A 0 -> (forall n, A n -> A (Nsucc n)) -> forall n, A n.
+Proof.
+intros A predicate_wd; apply Nind.
+Qed.
+
+Theorem pred_0 : Npred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem pred_succ : forall n : N, Npred (Nsucc n) = n.
+Proof.
+destruct n as [| p]; simpl. reflexivity.
+case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
+intro H; false_hyp H Psucc_not_one.
+Qed.
+
+Theorem plus_0_l : forall n : N, 0 + n = n.
+Proof Nplus_0_l.
+
+Theorem plus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m).
+Proof Nplus_succ.
+
+Theorem minus_0_r : forall n : N, n - 0 = n.
+Proof Nminus_0_r.
+
+Theorem minus_succ_r : forall n m : N, n - (S m) = P (n - m).
+Proof Nminus_succ_r.
+
+Theorem times_0_r : forall n : N, n * 0 = 0.
+Proof.
+intro n; rewrite Nmult_comm; apply Nmult_0_l.
+Qed.
+
+Theorem times_succ_r : forall n m : N, n * (Nsucc m) = n * m + n.
+Proof.
+intros n m; rewrite Nmult_comm, Nmult_Sn_m.
+now rewrite Nplus_comm, Nmult_comm.
+Qed.
+
+Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m.
+Proof.
+intros n m.
+assert (H : (n ?= m) = Eq <-> n = m).
+split; intro H; [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl].
+unfold Nle, Nlt. rewrite <- H.
+destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right.
+now elim H1. destruct H1; discriminate.
+Qed.
+
+Theorem nlt_0_r : forall n : N, ~ (n < 0).
 Proof.
-intros P predicate_wd; apply Nind.
+unfold Nlt; destruct n as [| p]; simpl; discriminate.
+Qed.
+
+Theorem lt_succ_le : forall n m : N, n < (S m) <-> n <= m.
+Proof.
+intros x y. rewrite le_lt_or_eq.
+unfold Nlt, Nle, S; apply Ncompare_n_Sm.
 Qed.
 
 Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
@@ -82,7 +174,7 @@ Qed.
 Theorem recursion_succ :
   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)).
+      forall n : N, EA (recursion a f (Nsucc 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.
@@ -90,8 +182,11 @@ clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
 now rewrite Nrect_step.
 Qed.
 
-End BinaryNat.
+End NBinaryAxiomsMod.
 
+Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod.
+
+(*
 Module NBinaryDepRec <: NDepRecSignature.
 Module Export NDomainModule := NBinaryDomain.
 Module Export NBaseMod := BinaryNat.
@@ -124,16 +219,6 @@ Proof.
 unfold E; congruence.
 Qed.
 
-Theorem plus_0_l : forall n, 0 + n = n.
-Proof.
-exact Nplus_0_l.
-Qed.
-
-Theorem plus_succ_l : forall n m, (S n) + m = S (n + m).
-Proof.
-exact Nplus_succ.
-Qed.
-
 End NBinaryPlus.
 
 Module NBinaryTimes <: NTimesSig.
@@ -146,16 +231,6 @@ Proof.
 unfold E; congruence.
 Qed.
 
-Theorem times_0_r : forall n, n * 0 = 0.
-Proof.
-intro n; rewrite Nmult_comm; apply Nmult_0_l.
-Qed.
-
-Theorem times_succ_r : forall n m, n * (S m) = n * m + n.
-Proof.
-intros n m; rewrite Nmult_comm; rewrite Nmult_succn_m.
-rewrite Nplus_comm; now rewrite Nmult_comm.
-Qed.
 
 End NBinaryTimes.
 
@@ -195,7 +270,7 @@ assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt);
 [unfold lt, comp_bool; destruct (x ?= S y); simpl; split; now intro |].
 assert (H2 : lt x y <-> Ncompare x y = Lt);
 [unfold lt, comp_bool; destruct (x ?= y); simpl; split; now intro |].
-pose proof (Ncompare_n_succm x y) as H. tauto.
+pose proof (Ncompare_n_Sm    m x y) as H. tauto.
 Qed.
 
 End NBinaryOrder.
@@ -227,7 +302,7 @@ end.
 *)
 (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
 
-
+*)
 (*
  Local Variables:
  tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0240f29b1..aa5ac99cf 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,66 +1,165 @@
-(*Require Import Minus.*)
-
-Require Export NPlus.
-(*Require Export NDepRec.
-Require Export NTimesOrder.
-Require Export NMinus.
-Require Export NMiscFunct.*)
-
-(* First we define the functions that will be suppled as
-implementations. The parameters in module types, to which these
-functions are going to be assigned, are declared Inline,
-so in the properties functors the definitions are going to
-be unfolded and the theorems proved in these functors
-will contain these functions in their statements. *)
-
-(* Decidable equality *)
-Fixpoint e (x y : nat) {struct x} : bool :=
-match x, y with
-| 0, 0 => true
-| S x', S y' => e x' y'
-| _, _ => false
-end.
+Require Import Arith.
+Require Import NMinus.
 
-(* The boolean < function can be defined as follows using the
-standard library:
+Module NPeanoAxiomsMod <: NAxiomsSig.
 
-fun n m => proj1_sig (nat_lt_ge_bool n m)
+Definition N := nat.
+Definition E := (@eq nat).
+Definition O := 0.
+Definition S := S.
+Definition P := pred.
+Definition plus := plus.
+Definition minus := minus.
+Definition times := mult.
+Definition lt := lt.
+Definition le := le.
+Definition recursion : forall A : Set, A -> (N -> A -> A) -> N -> A :=
+  fun A : Set => nat_rec (fun _ => A).
+Implicit Arguments recursion [A].
 
-However, this definition seems too complex. First, there are many
-functions involved: nat_lt_ge_bool is defined (in Coq.Arith.Bool_nat)
-using bool_of_sumbool and
+Theorem E_equiv : equiv nat E.
+Proof (eq_equiv nat).
 
-lt_ge_dec : forall x y : nat, {x < y} + {x >= y},
+Add Relation nat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
 
-where the latter function is defined using sumbool_not and
+(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat E"
+then the theorem generated for succ_wd below is forall x, succ x = succ x,
+which does not match the axioms in NAxiomsSig *)
 
-le_lt_dec : forall n m : nat, {n <= m} + {m < n}.
+Add Morphism S with signature E ==> E as succ_wd.
+Proof.
+congruence.
+Qed.
 
-Second, this definition is not the most efficient, especially since
-le_lt_dec is proved using tactics, not by giving the explicit proof
-term. *)
+Add Morphism P with signature E ==> E as pred_wd.
+Proof.
+congruence.
+Qed.
 
-Fixpoint lt (n m : nat) {struct n} : bool :=
-match n, m with
-| _, 0 => false
-| 0, S _ => true
-| S n', S m' => lt n' m'
-end.
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+congruence.
+Qed.
 
-Fixpoint le (n m : nat) {struct n} : bool :=
-match n, m with
-| 0, _ => true
-| S n', S m' => le n' m'
-| S _, 0 => false
-end.
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+congruence.
+Qed.
 
-Delimit Scope NatScope with Nat.
-Open Scope NatScope.
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+congruence.
+Qed.
 
-Module NPeanoBaseMod <: NBaseSig.
+Add Morphism lt with signature E ==> E ==> iff as lt_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
 
-Theorem E_equiv : equiv nat (@eq nat).
-Proof (eq_equiv nat).
+Add Morphism le with signature E ==> E ==> iff as le_wd.
+Proof.
+unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Theorem induction :
+  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
+    A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n.
+Proof.
+intros; now apply nat_ind.
+Qed.
+
+Theorem pred_0 : pred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem pred_succ : forall n : nat, pred (S n) = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem plus_0_l : forall n : nat, 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Theorem plus_succ_l : forall n m : nat, (S n) + m = S (n + m).
+Proof.
+reflexivity.
+Qed.
+
+Theorem minus_0_r : forall n : nat, n - 0 = n.
+Proof.
+intro n; now destruct n.
+Qed.
+
+Theorem minus_succ_r : forall n m : nat, n - (S m) = pred (n - m).
+Proof.
+intros n m; induction n m using nat_double_ind; simpl; auto. apply minus_0_r.
+Qed.
+
+Theorem times_0_r : forall n : nat, n * 0 = 0.
+Proof.
+exact mult_0_r.
+Qed.
+
+Theorem times_succ_r : forall n m : nat, n * (S m) = n * m + n.
+Proof.
+intros n m; symmetry; apply mult_n_Sm.
+Qed.
+
+Theorem le_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m.
+Proof.
+intros n m; split.
+apply le_lt_or_eq.
+intro H; destruct H as [H | H].
+now apply lt_le_weak. rewrite H; apply le_refl.
+Qed.
+
+Theorem nlt_0_r : forall n : nat, ~ (n < 0).
+Proof.
+exact lt_n_O.
+Qed.
+
+Theorem lt_succ_le : forall n m : nat, n < S m <-> n <= m.
+Proof.
+intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
+Qed.
+
+Theorem recursion_wd : forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 (@eq nat) EA EA f f' ->
+      forall n n' : N, n = n' ->
+        EA (recursion a f n) (recursion a' f' n').
+Proof.
+unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+Proof.
+reflexivity.
+Qed.
+
+Theorem recursion_succ :
+  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd (@eq nat) EA EA f ->
+      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+Proof.
+unfold eq_fun2; induction n; simpl; auto.
+Qed.
+
+End NPeanoAxiomsMod.
+
+(* Now we apply the largest property functor *)
+
+Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
+
+(*
 
 Theorem succ_wd : fun_wd (@eq nat) (@eq nat) S.
 Proof.
@@ -77,12 +176,6 @@ Proof.
 intros n H; simplify_eq H.
 Qed.
 
-Theorem induction :
-  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
-    A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n.
-Proof.
-intros; now apply nat_ind.
-Qed.
 
 Definition N := nat.
 Definition E := (@eq nat).
@@ -318,6 +411,7 @@ Qed.
 Add Ring SR : semi_ring (decidable e_implies_E).
 
 Goal forall x y : nat, x + y = y + x. intros. ring.*)
+*)
 
 
 (*
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index fd9e9aa8b..6d3ad55a9 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -134,6 +134,23 @@ let y := fresh "y" in
 let H := fresh "H" in
   intros x y H; qiff x y H.
 
+Ltac solve_rel_wd :=
+unfold rel_wd, fun2_wd;
+let x1 := fresh "x" in
+let y1 := fresh "y" in
+let H1 := fresh "H" in
+let x2 := fresh "x" in
+let y2 := fresh "y" in
+let H2 := fresh "H" in
+  intros x1 y1 H1 x2 y2 H2;
+  qsetoid_rewrite H1;
+  qiff x2 y2 H2.
+(* The tactic solve_rel_wd is not very efficient because qsetoid_rewrite
+uses qiff to take the formula apart in order to make it quantifier-free,
+and then qiff is called again and takes the formula apart for the second
+time. It is better to analyze the formula once and generalize qiff to take
+a list of equalities that it has to rewrite. *)
+
 (* The following tactic uses solve_predicate_wd to solve the goals
 relating to well-defidedness that are produced by applying induction.
 We declare it to take the tactic that applies the induction theorem
@@ -205,6 +222,10 @@ Ltac rewrite_false P H :=
 setoid_replace P with False using relation iff;
 [| apply -> neg_false; apply H].
 
+Ltac rewrite_true P H :=
+setoid_replace P with True using relation iff;
+[| split; intro; [constructor | apply H]].
+
 Tactic Notation "symmetry" constr(Eq) :=
 lazymatch Eq with
 | ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff;