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

12 files changed, 1962 insertions, 0 deletions

diff --git a/theories/Numbers/NatInt/Makefile b/theories/Numbers/NatInt/Makefile
new file mode 100644
index 0000000000..e23d8dee24
--- /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 0000000000..fa0bd21a35
--- /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 0000000000..64cf684896
--- /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 0000000000..f35e030e14
--- /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 0000000000..fd7cf608ad
--- /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 0000000000..f5b757a20f
--- /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 0000000000..6a15ddc6aa
--- /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 0000000000..d333274ba6
--- /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 0000000000..f43b549e20
--- /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 0000000000..2425224b86
--- /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 0000000000..ca78ced69e
--- /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 0000000000..95275f8c0e
--- /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:
+*)