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

10 files changed, 1469 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
new file mode 100644
index 0000000000..4019b47742
--- /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/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
new file mode 100644
index 0000000000..e0b753d4e6
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -0,0 +1,103 @@
+Require Export NumPrelude.
+Require Import NZBase.
+
+Module Type ZBaseSig.
+
+Parameter Z : Set.
+Parameter ZE : Z -> Z -> Prop.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Open Local Scope IntScope.
+
+Notation "x == y"  := (ZE x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ ZE x y) (at level 70) : 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.
+
+Parameter Z0 : Z.
+Parameter Zsucc : Z -> Z.
+
+Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
+
+Notation "0" := Z0 : IntScope.
+Notation "'S'" := Zsucc : IntScope.
+Notation "1" := (S 0) : IntScope.
+(* Note: if we put the line declaring 1 before the line declaring 'S' and
+change (S 0) to (Zsucc 0), then 1 will be parsed but not printed ((S 0)
+will be printed instead of 1) *)
+
+Axiom Zsucc_inj : forall x y : Z, S x == S y -> x == y.
+
+Axiom Zinduction :
+  forall A : predicate Z, predicate_wd ZE A ->
+    A 0 -> (forall x, A x <-> A (S x)) -> forall x, A x.
+
+End ZBaseSig.
+
+Module ZBasePropFunct (Import ZBaseMod : ZBaseSig).
+Open Local Scope IntScope.
+
+Module NZBaseMod <: NZBaseSig.
+
+Definition NZ := Z.
+Definition NZE := ZE.
+Definition NZ0 := Z0.
+Definition NZsucc := Zsucc.
+
+(* Axioms *)
+Definition NZE_equiv := ZE_equiv.
+
+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 Zsucc_wd.
+
+Definition NZsucc_inj := Zsucc_inj.
+Definition NZinduction := Zinduction.
+
+End NZBaseMod.
+
+Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
+
+Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
+Proof NZneq_symm.
+
+Theorem Zcentral_induction :
+  forall A : Z -> Prop, predicate_wd ZE A ->
+    forall z : Z, A z ->
+      (forall n : Z, A n <-> A (S n)) ->
+        forall n : Z, A n.
+Proof NZcentral_induction.
+
+Theorem Zsucc_inj_wd : forall n m, S n == S m <-> n == m.
+Proof NZsucc_inj_wd.
+
+Theorem Zsucc_inj_neg : forall n m, S n ~= S m <-> n ~= m.
+Proof NZsucc_inj_wd_neg.
+
+Tactic Notation "Zinduct" ident(n) :=
+  induction_maker n ltac:(apply Zinduction).
+(* FIXME: Zinduction probably has to be redeclared in the functor because
+the parameters like Zsucc are not unfolded for Zinduction in the signature *)
+
+Tactic Notation "Zinduct" ident(n) constr(z) :=
+  induction_maker n ltac:(apply Zcentral_induction with z).
+
+End ZBasePropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v
new file mode 100644
index 0000000000..9a7aaa099f
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDec.v
@@ -0,0 +1,8 @@
+Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
new file mode 100644
index 0000000000..028128cf7a
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -0,0 +1,62 @@
+Require Export NumPrelude.
+
+Module Type ZDomainSignature.
+
+Parameter Inline Z : Set.
+Parameter Inline E : Z -> Z -> Prop.
+Parameter Inline e : Z -> Z -> bool.
+
+Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
+Axiom E_equiv : equiv Z E.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y" := (E x y) (at level 70) : IntScope.
+Notation "x # y" := (~ E x y) (at level 70) : IntScope.
+
+End ZDomainSignature.
+
+Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
+Open Local Scope IntScope.
+
+Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
+Proof.
+intros x x' Exx' y y' Eyy'.
+case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
+assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
+assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
+rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
+assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
+assert (x == y); [rewrite Exx'; now rewrite Eyy' |
+rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
+Qed.
+
+Theorem neq_symm : forall n m, n # m -> m # n.
+Proof.
+intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+Qed.
+
+Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step ZE_stepl.
+
+(* The right step lemma is just transitivity of E *)
+Declare Right Step (proj1 (proj2 E_equiv)).
+
+End ZDomainProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
new file mode 100644
index 0000000000..cc834b442b
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -0,0 +1,458 @@
+Require Export ZAxioms.
+
+Module Type ZOrderSignature.
+Declare Module Export ZBaseMod : ZBaseSig.
+Open Local Scope IntScope.
+
+Parameter Inline lt : Z -> Z -> bool.
+Parameter Inline le : Z -> Z -> bool.
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+
+Notation "n <  m" := (lt n m) : IntScope.
+Notation "n <= m" := (le n m) : IntScope.
+
+Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m.
+Axiom lt_irr : forall n, ~ (n < n).
+Axiom lt_succ : forall n m, n < (S m) <-> n <= m.
+
+End ZOrderSignature.
+
+
+Module ZOrderProperties (Import ZOrderModule : ZOrderSignature).
+Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
+Open Local Scope IntScope.
+
+Ltac Zle_intro1 := rewrite le_lt; left.
+Ltac Zle_intro2 := rewrite le_lt; right.
+Ltac Zle_elim H := rewrite le_lt in H; destruct H as [H | H].
+
+Theorem le_refl : forall n, n <= n.
+Proof.
+intro n; now Zle_intro2.
+Qed.
+
+Theorem lt_n_succn : forall n, n < S n.
+Proof.
+intro n. rewrite lt_succ. now Zle_intro2.
+Qed.
+
+Theorem le_n_succn : forall n, n <= S n.
+Proof.
+intro; Zle_intro1; apply lt_n_succn.
+Qed.
+
+Theorem lt_predn_n : forall n, P n < n.
+Proof.
+intro n; rewrite_succ_pred n at 2; apply lt_n_succn.
+Qed.
+
+Theorem le_predn_n : forall n, P n <= n.
+Proof.
+intro; Zle_intro1; apply lt_predn_n.
+Qed.
+
+Theorem lt_n_succm : forall n m, n < m -> n < S m.
+Proof.
+intros. rewrite lt_succ. now Zle_intro1.
+Qed.
+
+Theorem le_n_succm : forall n m, n <= m -> n <= S m.
+Proof.
+intros n m H; rewrite <- lt_succ in H; now Zle_intro1.
+Qed.
+
+Theorem lt_n_m_pred : forall n m, n < m <-> n <= P m.
+Proof.
+intros n m; rewrite_succ_pred m; rewrite pred_succ; apply lt_succ.
+Qed.
+
+Theorem not_le_n_predn : forall n, ~ n <= P n.
+Proof.
+intros n H; Zle_elim H.
+apply lt_n_succm in H; rewrite succ_pred in H; false_hyp H lt_irr.
+pose proof (lt_predn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem le_succ : forall n m, n <= S m <-> n <= m \/ n == S m.
+Proof.
+intros n m; rewrite le_lt. now rewrite lt_succ.
+Qed.
+
+Theorem lt_pred : forall n m, (P n) < m <-> n <= m.
+Proof.
+intro n; induct_n m (P n).
+split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_predn.
+intros m IH; split; intro H.
+apply -> lt_succ in H; Zle_elim H.
+apply -> IH in H; now apply le_n_succm.
+rewrite <- H; rewrite succ_pred; now Zle_intro2.
+apply -> le_succ in H; destruct H as [H | H].
+apply <- IH in H. now apply lt_n_succm. rewrite H; rewrite pred_succ; apply lt_n_succn.
+intros m IH; split; intro H.
+pose proof H as H1. apply lt_n_succm in H; rewrite succ_pred in H.
+apply -> IH in H; Zle_elim H. now apply -> lt_n_m_pred.
+rewrite H in H1; false_hyp H1 lt_irr.
+pose proof H as H1. apply le_n_succm in H. rewrite succ_pred in H.
+apply <- IH in H. apply -> lt_n_m_pred in H. Zle_elim H.
+assumption. apply pred_inj in H; rewrite H in H1; false_hyp H1 not_le_n_predn.
+Qed.
+
+Theorem lt_predn_m : forall n m, n < m -> P n < m.
+Proof.
+intros; rewrite lt_pred; now Zle_intro1.
+Qed.
+
+Theorem le_predn_m : forall n m, n <= m -> P n <= m.
+Proof.
+intros n m H; rewrite <- lt_pred in H; now Zle_intro1.
+Qed.
+
+Theorem lt_n_m_succ : forall n m, n < m <-> S n <= m.
+Proof.
+intros n m; rewrite_pred_succ n; rewrite succ_pred; apply lt_pred.
+Qed.
+
+Theorem lt_succn_m : forall n m, S n < m -> n < m.
+Proof.
+intros n m H; rewrite_pred_succ n; now apply lt_predn_m.
+Qed.
+
+Theorem le_succn_m : forall n m, S n <= m -> n <= m.
+Proof.
+intros n m H; rewrite <- lt_n_m_succ in H; now Zle_intro1.
+Qed.
+
+Theorem lt_n_predm : forall n m, n < P m -> n < m.
+Proof.
+intros n m H; rewrite_succ_pred m; now apply lt_n_succm.
+Qed.
+
+Theorem le_n_predm : forall n m, n <= P m -> n <= m.
+Proof.
+intros n m H; rewrite <- lt_n_m_pred in H; now Zle_intro1.
+Qed.
+
+Theorem lt_respects_succ : forall n m, n < m <-> S n < S m.
+Proof.
+intros n m. rewrite lt_n_m_succ. symmetry. apply lt_succ.
+Qed.
+
+Theorem le_respects_succ : forall n m, n <= m <-> S n <= S m.
+Proof.
+intros n m. do 2 rewrite le_lt.
+firstorder using lt_respects_succ succ_wd succ_inj.
+Qed.
+
+Theorem lt_respects_pred : forall n m, n < m <-> P n < P m.
+Proof.
+intros n m. rewrite lt_n_m_pred. symmetry; apply lt_pred.
+Qed.
+
+Theorem le_respects_pred : forall n m, n <= m <-> P n <= P m.
+Proof.
+intros n m. do 2 rewrite le_lt.
+firstorder using lt_respects_pred pred_wd pred_inj.
+Qed.
+
+Theorem lt_succ_pred : forall n m, S n < m <-> n < P m.
+Proof.
+intros n m; rewrite_pred_succ n at 2; apply lt_respects_pred.
+Qed.
+
+Theorem le_succ_pred : forall n m, S n <= m <-> n <= P m.
+Proof.
+intros n m; rewrite_pred_succ n at 2; apply le_respects_pred.
+Qed.
+
+Theorem lt_pred_succ : forall n m, P n < m <-> n < S m.
+Proof.
+intros n m; rewrite_succ_pred n at 2; apply lt_respects_succ.
+Qed.
+
+Theorem le_pred_succ : forall n m, P n <= m <-> n <= S m.
+Proof.
+intros n m; rewrite_succ_pred n at 2; apply le_respects_succ.
+Qed.
+
+Theorem lt_neq : forall n m, n < m -> n # m.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
+Proof.
+intros n m; induct_n n m.
+intros p H _; false_hyp H lt_irr.
+intros n IH p H1 H2. apply lt_succn_m in H1. pose proof (IH p H1 H2) as H3.
+rewrite lt_n_m_succ in H3; Zle_elim H3.
+assumption. rewrite <- H3 in H2. rewrite lt_succ in H2; Zle_elim H2.
+elimtype False; apply lt_irr with (n := n); now apply IH.
+rewrite H2 in H1; false_hyp H1 lt_irr.
+intros n IH p H1 H2. apply lt_predn_m. rewrite lt_pred in H1; Zle_elim H1.
+now apply IH. now rewrite H1.
+Qed.
+
+Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p H1 H2; Zle_elim H1.
+Zle_elim H2. Zle_intro1; now apply lt_trans with (m := m).
+Zle_intro1; now rewrite <- H2. now rewrite H1.
+Qed.
+
+Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; Zle_elim H1.
+now apply lt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; Zle_elim H2.
+now apply lt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem lt_asymm : forall n m, n < m -> ~ m < n.
+Proof.
+intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+Qed.
+
+Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m.
+Proof.
+intros n m H1 H2; Zle_elim H1; Zle_elim H2.
+elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+now symmetry. assumption. assumption.
+Qed.
+
+Theorem not_lt_succn_n : forall n, ~ S n < n.
+Proof.
+intros n H; apply (lt_asymm n (S n)). apply lt_n_succn. assumption.
+Qed.
+
+Theorem not_le_succn_n : forall n, ~ S n <= n.
+Proof.
+intros n H; Zle_elim H. false_hyp H not_lt_succn_n.
+pose proof (lt_n_succn n) as H1. rewrite H in H1; false_hyp H1 lt_irr.
+Qed.
+
+Theorem lt_gt : forall n m, n < m -> m < n -> False.
+Proof.
+intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+Qed.
+
+Theorem lt_total : forall n m,  n < m \/ n == m \/ m < n.
+Proof.
+intros n m; induct_n n m.
+right; now left.
+intros n IH; destruct IH as [H | [H | H]].
+rewrite lt_n_m_succ in H. rewrite le_lt in H; tauto.
+right; right; rewrite H; apply lt_n_succn.
+right; right; now apply lt_n_succm.
+intros n IH; destruct IH as [H | [H | H]].
+left; now apply lt_predn_m.
+left; rewrite H; apply lt_predn_n.
+rewrite lt_n_m_pred in H. rewrite le_lt in H.
+setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto.
+split; intro; now symmetry.
+Qed.
+
+Theorem le_gt : forall n m, n <= m <-> ~ m < n.
+Proof.
+intros n m. rewrite -> le_lt.
+pose proof (lt_total n m). pose proof (lt_gt n m).
+assert (n == m -> ~ m < n); [intro A; rewrite A; apply lt_irr |].
+tauto.
+Qed.
+
+Theorem lt_ge : forall n m, n < m <-> ~ m <= n.
+Proof.
+intros n m. rewrite -> le_lt.
+pose proof (lt_total m n). pose proof (lt_gt n m).
+assert (n < m -> m # n); [intros A B; rewrite B in A; false_hyp A lt_irr |].
+tauto.
+Qed.
+
+Theorem lt_discrete : forall n m, n < m -> m < S n -> False.
+Proof.
+intros n m H1 H2; apply -> lt_succ in H2; apply -> lt_ge in H1; false_hyp H2 H1.
+Qed.
+
+(* Decidability of order can be proved either from totality or from the fact
+that < and <= are boolean functions *)
+
+(** A corollary of having an order is that Z is infinite in both
+directions *)
+
+Theorem neq_succn_n : forall n, S n # n.
+Proof.
+intros n H. pose proof (lt_n_succn n) as H1. rewrite H in H1. false_hyp H1 lt_irr.
+Qed.
+
+Theorem neq_predn_n : forall n, P n # n.
+Proof.
+intros n H. apply succ_wd in H. rewrite succ_pred in H. now apply neq_succn_n with (n := n).
+Qed.
+
+Definition nth_succ (n : nat) (m : Z) :=
+  nat_rec (fun _ => Z) m (fun _ l => S l) n.
+Definition nth_pred (n : nat) (m : Z) :=
+  nat_rec (fun _ => Z) m (fun _ l => P l) n.
+
+Lemma lt_m_succkm :
+  forall (n : nat) (m : Z), m < nth_succ (Datatypes.S n) m.
+Proof.
+intros n m; induction n as [| n IH]; simpl in *.
+apply lt_n_succn. now apply lt_n_succm.
+Qed.
+
+Lemma lt_predkm_m :
+  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m < m.
+Proof.
+intros n m; induction n as [| n IH]; simpl in *.
+apply lt_predn_n. now apply lt_predn_m.
+Qed.
+
+Theorem neq_m_succkm :
+  forall (n : nat) (m : Z), nth_succ (Datatypes.S n) m # m.
+Proof.
+intros n m H. pose proof (lt_m_succkm n m) as H1. rewrite H in H1.
+false_hyp H1 lt_irr.
+Qed.
+
+Theorem neq_predkm_m :
+  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m # m.
+Proof.
+intros n m H. pose proof (lt_predkm_m n m) as H1. rewrite H in H1.
+false_hyp H1 lt_irr.
+Qed.
+
+(** Stronger variant of induction with assumptions n >= 0 (n <= 0)
+in the induction step *)
+
+Section Induction.
+
+Variable A : Z -> Prop.
+Hypothesis Q_wd : predicate_wd E A.
+
+Add Morphism A with signature E ==> 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, z <= m -> m < n -> A m.
+
+Add Morphism Q' with signature E ==> iff as Q'_pos_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem right_induction :
+  A z -> (forall n, z <= n -> A n -> A (S n)) -> forall n, z <= n -> A n.
+Proof.
+intros Qz QS k k_ge_z.
+assert (H : forall n, Q' n). induct_n n z; unfold Q'.
+intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
+intros n IH m H2 H3.
+rewrite lt_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 lt_predn_n. 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 lt_n_succn.
+Qed.
+
+End RightInduction.
+
+Section LeftInduction.
+
+Let Q' := fun n : Z => forall m, m <= z -> n < m -> A m.
+
+Add Morphism Q' with signature E ==> iff as Q'_neg_wd.
+Proof.
+intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+Qed.
+
+Theorem left_induction :
+  A z -> (forall n, n <= z -> A n -> A (P n)) -> forall n, n <= z -> A n.
+Proof.
+intros Qz QP k k_le_z.
+assert (H : forall n, Q' n). induct_n n z; unfold Q'.
+intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
+intros n IH m H2 H3. apply IH. assumption. now apply lt_succn_m.
+intros n IH m H2 H3.
+rewrite lt_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 lt_n_succn. now rewrite H2.
+pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
+apply k_le_z. apply lt_predn_n.
+Qed.
+
+End LeftInduction.
+
+Theorem induction_ord_n :
+  A z ->
+  (forall n, z <= n -> A n -> A (S n)) ->
+  (forall n, n <= z -> A n -> A (P n)) ->
+    forall n, 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 induction_ord :
+  A 0 ->
+  (forall n, 0 <= n -> A n -> A (S n)) ->
+  (forall n, n <= 0 -> A n -> A (P n)) ->
+    forall n, A n.
+Proof (induction_ord_n 0).
+
+Theorem lt_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 le_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/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
new file mode 100644
index 0000000000..624f85f043
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -0,0 +1,228 @@
+Require Export ZAxioms.
+
+Module Type ZPlusSignature.
+Declare Module Export ZBaseMod : ZBaseSig.
+Open Local Scope IntScope.
+
+Parameter Inline plus : Z -> Z -> Z.
+Parameter Inline minus : Z -> Z -> Z.
+Parameter Inline uminus : Z -> Z.
+
+Notation "x + y" := (plus x y) : IntScope.
+Notation "x - y" := (minus x y) : IntScope.
+Notation "- x" := (uminus x) : IntScope.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Add Morphism uminus with signature E ==> E as uminus_wd.
+
+Axiom plus_0 : forall n, 0 + n == n.
+Axiom plus_succ : forall n m, (S n) + m == S (n + m).
+
+Axiom minus_0 : forall n, n - 0 == n.
+Axiom minus_succ : forall n m, n - (S m) == P (n - m).
+
+Axiom uminus_0 : - 0 == 0.
+Axiom uminus_succ : forall n, - (S n) == P (- n).
+
+End ZPlusSignature.
+
+Module ZPlusProperties (Import ZPlusModule : ZPlusSignature).
+Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
+Open Local Scope IntScope.
+
+Theorem plus_pred : forall n m, P n + m == P (n + m).
+Proof.
+intros n m. rewrite_succ_pred n at 2. rewrite plus_succ. now rewrite pred_succ.
+Qed.
+
+Theorem minus_pred : forall n m, n - (P m) == S (n - m).
+Proof.
+intros n m. rewrite_succ_pred m at 2. rewrite minus_succ. now rewrite succ_pred.
+Qed.
+
+Theorem uminus_pred : forall n, - (P n) == S (- n).
+Proof.
+intro n. rewrite_succ_pred n at 2. rewrite uminus_succ. now rewrite succ_pred.
+Qed.
+
+Theorem plus_n_0 : forall n, n + 0 == n.
+Proof.
+induct n.
+now rewrite plus_0.
+intros n IH. rewrite plus_succ. now rewrite IH.
+intros n IH. rewrite plus_pred. now rewrite IH.
+Qed.
+
+Theorem plus_n_succm : forall n m, n + S m == S (n + m).
+Proof.
+intros n m; induct n.
+now do 2 rewrite plus_0.
+intros n IH. do 2 rewrite plus_succ. now rewrite IH.
+intros n IH. do 2 rewrite plus_pred. rewrite IH. rewrite pred_succ; now rewrite succ_pred.
+Qed.
+
+Theorem plus_n_predm : forall n m, n + P m == P (n + m).
+Proof.
+intros n m; rewrite_succ_pred m at 2. rewrite plus_n_succm; now rewrite pred_succ.
+Qed.
+
+Theorem plus_opp_minus : forall n m, n + (- m) == n - m.
+Proof.
+induct m.
+rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0.
+intros m IH. rewrite uminus_succ; rewrite minus_succ. rewrite plus_n_predm; now rewrite IH.
+intros m IH. rewrite uminus_pred; rewrite minus_pred. rewrite plus_n_succm; now rewrite IH.
+Qed.
+
+Theorem minus_0_n : forall n, 0 - n == - n.
+Proof.
+intro n; rewrite <- plus_opp_minus; now rewrite plus_0.
+Qed.
+
+Theorem minus_succn_m : forall n m, S n - m == S (n - m).
+Proof.
+intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_succ.
+Qed.
+
+Theorem minus_predn_m : forall n m, P n - m == P (n - m).
+Proof.
+intros n m. rewrite_succ_pred n at 2; rewrite minus_succn_m; now rewrite pred_succ.
+Qed.
+
+Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
+Proof.
+intros n m p; induct n.
+now do 2 rewrite plus_0.
+intros n IH. do 3 rewrite plus_succ. now rewrite IH.
+intros n IH. do 3 rewrite plus_pred. now rewrite IH.
+Qed.
+
+Theorem plus_comm : forall n m, n + m == m + n.
+Proof.
+intros n m; induct n.
+rewrite plus_0; now rewrite plus_n_0.
+intros n IH; rewrite plus_succ; rewrite plus_n_succm; now rewrite IH.
+intros n IH; rewrite plus_pred; rewrite plus_n_predm; now rewrite IH.
+Qed.
+
+Theorem minus_diag : forall n, n - n == 0.
+Proof.
+induct n.
+now rewrite minus_0.
+intros n IH. rewrite minus_succ; rewrite minus_succn_m; rewrite pred_succ; now rewrite IH.
+intros n IH. rewrite minus_pred; rewrite minus_predn_m; rewrite succ_pred; now rewrite IH.
+Qed.
+
+Theorem plus_opp_r : forall n, n + (- n) == 0.
+Proof.
+intro n; rewrite plus_opp_minus; now rewrite minus_diag.
+Qed.
+
+Theorem plus_opp_l : forall n, - n + n == 0.
+Proof.
+intro n; rewrite plus_comm; apply plus_opp_r.
+Qed.
+
+Theorem minus_swap : forall n m, - m + n == n - m.
+Proof.
+intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm.
+Qed.
+
+Theorem plus_minus_inverse : forall n m, n + (m - n) == m.
+Proof.
+intros n m; rewrite <- minus_swap. rewrite plus_assoc;
+rewrite plus_opp_r; now rewrite plus_0.
+Qed.
+
+Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p.
+Proof.
+intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc.
+Qed.
+
+Theorem double_opp : forall n, - (- n) == n.
+Proof.
+induct n.
+now do 2 rewrite uminus_0.
+intros n IH. rewrite uminus_succ; rewrite uminus_pred; now rewrite IH.
+intros n IH. rewrite uminus_pred; rewrite uminus_succ; now rewrite IH.
+Qed.
+
+Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m).
+Proof.
+intros n m; induct n.
+rewrite uminus_0; now do 2 rewrite plus_0.
+intros n IH. rewrite plus_succ; do 2 rewrite uminus_succ. rewrite IH. now rewrite plus_pred.
+intros n IH. rewrite plus_pred; do 2 rewrite uminus_pred. rewrite IH. now rewrite plus_succ.
+Qed.
+
+Theorem opp_minus_distr : forall n m, - (n - m) == - n + m.
+Proof.
+intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr.
+now rewrite double_opp.
+Qed.
+
+Theorem opp_inj : forall n m, - n == - m -> n == m.
+Proof.
+intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H.
+Qed.
+
+Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p.
+Proof.
+intros n m p; rewrite <- plus_opp_minus. rewrite opp_plus_distr. rewrite plus_assoc.
+now do 2 rewrite plus_opp_minus.
+Qed.
+
+Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p.
+Proof.
+intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc.
+now rewrite plus_opp_minus.
+Qed.
+
+Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m.
+Proof.
+intros n m p. rewrite <- plus_minus_distr.
+rewrite <- (plus_opp_minus n p). rewrite <- plus_assoc. now rewrite minus_swap.
+Qed.
+
+Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p.
+Proof.
+intros n m p H.
+assert (H1 : - n + n + m == -n + n + p).
+do 2 rewrite <- plus_assoc; now rewrite H.
+rewrite plus_opp_l in H1; now do 2 rewrite plus_0 in H1.
+Qed.
+
+Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p.
+Proof.
+intros n m p H.
+rewrite plus_comm in H. set (k := m + n) in H. rewrite plus_comm in H.
+unfold k in H; clear k. now apply plus_cancel_l with m.
+Qed.
+
+Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m.
+Proof.
+intros n m p H.
+assert (H1 : - m + m + p == - m + n).
+rewrite <- plus_assoc; now rewrite H.
+rewrite plus_opp_l in H1. rewrite plus_0 in H1. now rewrite minus_swap in H1.
+Qed.
+
+Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p.
+Proof.
+intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H.
+Qed.
+
+Lemma minus_eq : forall n m, n - m == 0 -> n == m.
+Proof.
+intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
+Qed.
+
+End ZPlusProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
new file mode 100644
index 0000000000..95f0fa8c64
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -0,0 +1,167 @@
+Require Export ZOrder.
+Require Export ZPlus.
+
+Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature)
+                            (Import ZOrderModule : ZOrderSignature with
+                              Module ZBaseMod := ZPlusModule.ZBaseMod).
+Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
+Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule.
+(* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *)
+Open Local Scope IntScope.
+
+Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
+Proof.
+intros n m p; induct p.
+now do 2 rewrite plus_0.
+intros p IH. do 2 rewrite plus_succ. now rewrite <- lt_respects_succ.
+intros p IH. do 2 rewrite plus_pred. now rewrite <- lt_respects_pred.
+Qed.
+
+Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p.
+Proof.
+intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
+apply plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; do 2 rewrite <- lt_succ. rewrite <- plus_n_succm;
+apply plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
+apply plus_le_compat_l.
+Qed.
+
+Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. apply lt_trans with (m := m + p).
+now apply -> plus_lt_compat_r. now apply -> plus_lt_compat_l.
+Qed.
+
+Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat.
+rewrite H2. now apply -> plus_lt_compat_r.
+Qed.
+
+Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat.
+rewrite H1. now apply -> plus_lt_compat_l.
+Qed.
+
+Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2. Zle_elim H1. Zle_intro1; now apply plus_lt_le_compat.
+rewrite H1. now apply -> plus_le_compat_l.
+Qed.
+
+Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof.
+intros; rewrite <- (plus_0 0); now apply plus_le_compat.
+Qed.
+
+Lemma lt_opp_forward : forall n m, n < m -> - m < - n.
+Proof.
+induct n.
+induct_ord m.
+intro H; false_hyp H lt_irr.
+intros m H1 IH H2. rewrite uminus_succ. rewrite uminus_0 in *.
+Zle_elim H1. apply IH in H1. now apply lt_predn_m.
+rewrite <- H1; rewrite uminus_0; apply lt_predn_n.
+intros m H1 IH H2. apply lt_n_predm in H2. apply -> le_gt in H1. false_hyp H2 H1.
+intros n IH m H. rewrite uminus_succ.
+apply -> lt_succ_pred in H. apply IH in H. rewrite uminus_pred in H. now apply -> lt_succ_pred.
+intros n IH m H. rewrite uminus_pred.
+apply -> lt_pred_succ in H. apply IH in H. rewrite uminus_succ in H. now apply -> lt_pred_succ.
+Qed.
+
+Theorem lt_opp : forall n m, n < m <-> - m < - n.
+Proof.
+intros n m; split.
+apply lt_opp_forward.
+intro; rewrite <- (double_opp n); rewrite <- (double_opp m);
+now apply lt_opp_forward.
+Qed.
+
+Theorem le_opp : forall n m, n <= m <-> - m <= - n.
+Proof.
+intros n m; do 2 rewrite -> le_lt; rewrite <- lt_opp.
+assert (n == m <-> - m == - n).
+split; intro; [now apply uminus_wd | now apply opp_inj].
+tauto.
+Qed.
+
+Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply lt_opp. now rewrite uminus_0.
+Qed.
+
+Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply le_opp. now rewrite uminus_0.
+Qed.
+
+Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply lt_opp. now rewrite uminus_0.
+Qed.
+
+Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0.
+Proof.
+intro n. set (k := 0) in |-* at 2.
+setoid_replace k with (- k); unfold k; clear k.
+apply le_opp. now rewrite uminus_0.
+Qed.
+
+Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l.
+apply lt_opp.
+Qed.
+
+Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l.
+apply le_opp.
+Qed.
+
+Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r.
+Qed.
+
+Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p.
+Proof.
+intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r.
+Qed.
+
+Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p.
+Proof.
+intros n m p. rewrite (minus_lt_incr_l (n + p) m p).
+rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p.
+Proof.
+intros n m p. rewrite (minus_le_nondecr_l (n + p) m p).
+rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+End ZPlusOrderProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v
new file mode 100644
index 0000000000..ffcb2dea8a
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZPred.v
@@ -0,0 +1,60 @@
+Axiom succ_pred : forall x : Z, S (P x) == x.
+Add Morphism P with signature E ==> E as pred_wd.
+
+Theorem pred_inj : forall x y, P x == P y -> x == y.
+Proof.
+intros x y H.
+setoid_replace x with (S (P x)); [| symmetry; apply succ_pred].
+setoid_replace y with (S (P y)); [| symmetry; apply succ_pred].
+now rewrite H.
+Qed.
+
+Theorem pred_succ : forall x, P (S x) == x.
+Proof.
+intro x.
+apply succ_inj.
+now rewrite succ_pred.
+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 (succ_pred or pred_succ) 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 (A x) into (A (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_succP 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_succ_pred" constr(t) :=
+rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred.
+
+Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) :=
+rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred.
+
+Tactic Notation "rewrite_pred_succ" constr(t) :=
+rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ.
+
+Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) :=
+rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ.
+
+(* 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. *)
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
new file mode 100644
index 0000000000..38311aa2b4
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -0,0 +1,127 @@
+Require Export ZPlus.
+
+Module Type ZTimesSignature.
+Declare Module Export ZPlusModule : ZPlusSignature.
+Open Local Scope IntScope.
+
+Parameter Inline times : Z -> Z -> Z.
+
+Notation "x * y" := (times x y) : IntScope.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+
+Axiom times_0 : forall n, n * 0 == 0.
+Axiom times_succ : forall n m, n * (S m) == n * m + n.
+
+End ZTimesSignature.
+
+Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
+Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
+Open Local Scope IntScope.
+
+Theorem times_pred : forall n m, n * (P m) == n * m - n.
+Proof.
+intros n m. rewrite_succ_pred m at 2. rewrite times_succ. rewrite <- plus_minus_distr.
+rewrite minus_diag. now rewrite plus_n_0.
+Qed.
+
+Theorem times_0_n : forall n, 0 * n == 0.
+Proof.
+induct n.
+now rewrite times_0.
+intros n IH. rewrite times_succ. rewrite IH; now rewrite plus_0.
+intros n IH. rewrite times_pred. rewrite IH; now rewrite minus_0.
+Qed.
+
+Theorem times_succn_m : forall n m, (S n) * m == n * m + m.
+Proof.
+induct m.
+do 2 rewrite times_0. now rewrite plus_0.
+intros m IH. do 2 rewrite times_succ. rewrite IH.
+do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity.
+do 2 rewrite plus_n_succm; now rewrite plus_comm.
+intros m IH. do 2 rewrite times_pred. rewrite IH.
+rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr.
+apply plus_wd. reflexivity.
+rewrite minus_succ. now rewrite minus_predn_m.
+Qed.
+
+Theorem times_predn_m : forall n m, (P n) * m == n * m - m.
+Proof.
+intros n m. rewrite_succ_pred n at 2. rewrite times_succn_m.
+rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0.
+Qed.
+
+Theorem times_comm : forall n m, n * m == m * n.
+Proof.
+intros n m; induct n.
+rewrite times_0_n; now rewrite times_0.
+intros n IH. rewrite times_succn_m; rewrite times_succ; now rewrite IH.
+intros n IH. rewrite times_predn_m; rewrite times_pred; now rewrite IH.
+Qed.
+
+Theorem times_opp_r : forall n m, n * (- m) == - (n * m).
+Proof.
+intros n m; induct m.
+rewrite uminus_0; rewrite times_0; now rewrite uminus_0.
+intros m IH. rewrite uminus_succ. rewrite times_pred; rewrite times_succ. rewrite IH.
+rewrite <- plus_opp_minus; now rewrite opp_plus_distr.
+intros m IH. rewrite uminus_pred. rewrite times_pred; rewrite times_succ. rewrite IH.
+now rewrite opp_minus_distr.
+Qed.
+
+Theorem times_opp_l : forall n m, (- n) * m == - (n * m).
+Proof.
+intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m);
+now rewrite times_opp_r.
+Qed.
+
+Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m.
+Proof.
+intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp.
+Qed.
+
+Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p.
+Proof.
+intros n m p; induct m.
+rewrite times_0; now do 2 rewrite plus_0.
+intros m IH. rewrite plus_succ. do 2 rewrite times_succ. rewrite IH.
+do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm].
+intros m IH. rewrite plus_pred. do 2 rewrite times_pred. rewrite IH.
+apply plus_minus_swap.
+Qed.
+
+Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p.
+Proof.
+intros n m p; rewrite (times_comm (n + m) p); rewrite times_plus_distr_r;
+rewrite (times_comm p n); now rewrite (times_comm p m).
+Qed.
+
+Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p.
+Proof.
+intros n m p.
+do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r.
+Qed.
+
+Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p.
+Proof.
+intros n m p.
+do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l.
+Qed.
+
+Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
+Proof.
+intros n m p; induct p.
+now do 3 rewrite times_0.
+intros p IH. do 2 rewrite times_succ. rewrite times_plus_distr_r. now rewrite IH.
+intros p IH. do 2 rewrite times_pred. rewrite times_minus_distr_r. now rewrite IH.
+Qed.
+
+End ZTimesProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
new file mode 100644
index 0000000000..055342bcc1
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -0,0 +1,96 @@
+Require Export ZTimes.
+Require Export ZPlusOrder.
+
+Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature)
+                             (Import ZOrderModule : ZOrderSignature with
+                               Module ZBaseMod := ZTimesModule.ZPlusModule.ZBaseMod).
+Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule.
+Module Export ZPlusOrderPropertiesModule :=
+  ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule.
+Open Local Scope IntScope.
+
+Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p.
+Proof.
+intros n m p; induct_ord p.
+intros H _; false_hyp H lt_irr.
+intros p H IH H1 H2. do 2 rewrite times_succ.
+apply -> lt_succ in H1; Zle_elim H1.
+apply plus_lt_compat. now apply IH. assumption.
+rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0.
+intros p H IH H1 H2. apply lt_n_predm in H1. apply -> le_gt in H.
+false_hyp H1 H.
+Qed.
+
+Theorem mult_lt_compat_l : forall n m p, 0 < p -> n < m -> p * n < p * m.
+Proof.
+intros n m p. rewrite (times_comm p n); rewrite (times_comm p m).
+apply mult_lt_compat_r.
+Qed.
+
+Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p.
+Proof.
+intros n m p H1 H2; Zle_elim H2.
+Zle_intro1; now apply mult_lt_compat_r.
+rewrite H2. now Zle_intro2.
+Qed.
+
+Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m.
+Proof.
+intros n m p. rewrite (times_comm p n); rewrite (times_comm p m).
+apply mult_lt_le_compat_r.
+Qed.
+
+(* And so on *)
+
+Theorem mult_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
+Proof.
+intros n m; set (k := 0) in |-* at 3;
+setoid_replace k with (n * 0); unfold k; clear k.
+apply mult_lt_compat_l. now rewrite times_0.
+Qed.
+
+Theorem mult_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0.
+Proof.
+intros n m; set (k := 0) in |-* at 3;
+setoid_replace k with (n * 0); unfold k; clear k.
+apply mult_lt_compat_l. now rewrite times_0.
+Qed.
+(* The same proof script as for mult_pos_pos! *)
+
+Theorem mult_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0.
+Proof.
+intros n m H1 H2; rewrite times_comm; now apply mult_pos_neg.
+Qed.
+
+Theorem mult_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m.
+Proof.
+intros n m H1 H2. setoid_replace (n * m) with (- - (n * m));
+[| symmetry; apply double_opp].
+rewrite <- times_opp_l. rewrite <- times_opp_r.
+apply -> lt_opp_neg in H1. apply -> lt_opp_neg in H2.
+now apply mult_pos_pos.
+Qed.
+
+(** With order, Z is an integral domain *)
+Theorem mult_neq_0 : forall n m, n # 0 -> m # 0 -> n * m # 0.
+Proof.
+intros n m H1 H2.
+destruct (lt_total n 0) as [H3 | [H3 | H3]];
+destruct (lt_total m 0) as [H4 | [H4 | H4]].
+apply neq_symm. apply lt_neq. now apply mult_neg_neg.
+false_hyp H4 H2.
+apply lt_neq; now apply mult_neg_pos.
+false_hyp H3 H1. false_hyp H3 H1. false_hyp H3 H1.
+apply lt_neq; now apply mult_pos_neg.
+false_hyp H4 H2.
+apply neq_symm. apply lt_neq. now apply mult_pos_pos.
+Qed.
+
+End ZTimesOrderProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)