Added the compilation of theories/Numbers to Makefile.common. The following things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers.

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

46 files changed, 1034 insertions, 1363 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index d3c0410ea..ab863eb1f 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -10,14 +10,17 @@ Open Local Scope NatIntScope.
 Notation Z := NZ (only parsing).
 Notation E := NZE (only parsing).
 
-(** Integers are obtained by postulating that every number has a predecessor *)
-Axiom S_P : forall n : Z, S (P n) == n.
+Parameter Inline Zopp : Z -> Z.
 
-End ZAxiomsSig.
+Add Morphism Zopp with signature E ==> E as Zopp_wd.
+
+Notation "- x" := (Zopp x) (at level 35, right associativity) : NatIntScope.
+
+(* Integers are obtained by postulating that every number has a predecessor *)
+Axiom Zsucc_pred : forall n : Z, S (P n) == n.
 
+Axiom Zopp_0 : - 0 == 0.
+Axiom Zopp_succ : forall n : Z, - (S n) == P (- n).
+
+End ZAxiomsSig.
 
-(*
- 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
index 8f5c284e7..9f5ff8bd3 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -6,6 +6,9 @@ Open Local Scope NatIntScope.
 
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
+Theorem Zpred_succ : forall n : Z, P (S n) == n.
+Proof NZpred_succ.
+
 Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
 Proof NZneq_symm.
 
@@ -25,10 +28,17 @@ forall A : Z -> Prop, predicate_wd E A ->
       forall n : Z, A n.
 Proof NZcentral_induction.
 
+(* Theorems that are true for integers but not for natural numbers *)
+
+Theorem Zpred_inj : forall n m : Z, P n == P m -> n == m.
+Proof.
+intros n m H. apply NZsucc_wd in H. now do 2 rewrite Zsucc_pred in H.
+Qed.
+
+Theorem Zpred_inj_wd : forall n1 n2 : Z, P n1 == P n2 <-> n1 == n2.
+Proof.
+intros n1 n2; split; [apply Zpred_inj | apply NZpred_wd].
+Qed.
+
 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
index 9a7aaa099..843b48b93 100644
--- a/theories/Numbers/Integer/Abstract/ZDec.v
+++ b/theories/Numbers/Integer/Abstract/ZDec.v
@@ -1,8 +1,3 @@
 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
index 028128cf7..7ace860f3 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -55,8 +55,3 @@ 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
index cc834b442..295f5355a 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -1,458 +1,296 @@
-Require Export ZAxioms.
+Require Export ZTimes.
 
-Module Type ZOrderSignature.
-Declare Module Export ZBaseMod : ZBaseSig.
-Open Local Scope IntScope.
+Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
+Open Local Scope NatIntScope.
 
-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.
+(* Axioms *)
 
-Notation "n <  m" := (lt n m) : IntScope.
-Notation "n <= m" := (le n m) : IntScope.
+Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof NZle_lt_or_eq.
 
-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.
+Theorem Zlt_irrefl : forall n : Z, ~ n < n.
+Proof NZlt_irrefl.
 
-End ZOrderSignature.
+Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
+Proof NZlt_succ_le.
 
+(* Renaming theorems from NZOrder.v *)
 
-Module ZOrderProperties (Import ZOrderModule : ZOrderSignature).
-Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
-Open Local Scope IntScope.
+Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
+Proof NZlt_le_incl.
 
-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 Zlt_neq : forall n m : Z, n < m -> n ~= m.
+Proof NZlt_neq.
 
-Theorem le_refl : forall n, n <= n.
-Proof.
-intro n; now Zle_intro2.
-Qed.
+Theorem Zle_refl : forall n : Z, n <= n.
+Proof NZle_refl.
 
-Theorem lt_n_succn : forall n, n < S n.
-Proof.
-intro n. rewrite lt_succ. now Zle_intro2.
-Qed.
+Theorem Zlt_succ_r : forall n : Z, n < S n.
+Proof NZlt_succ_r.
 
-Theorem le_n_succn : forall n, n <= S n.
-Proof.
-intro; Zle_intro1; apply lt_n_succn.
-Qed.
+Theorem Zle_succ_r : forall n : Z, n <= S n.
+Proof NZle_succ_r.
 
-Theorem lt_predn_n : forall n, P n < n.
-Proof.
-intro n; rewrite_succ_pred n at 2; apply lt_n_succn.
-Qed.
+Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m.
+Proof NZlt_lt_succ.
 
-Theorem le_predn_n : forall n, P n <= n.
-Proof.
-intro; Zle_intro1; apply lt_predn_n.
-Qed.
+Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m.
+Proof NZle_le_succ.
 
-Theorem lt_n_succm : forall n m, n < m -> n < S m.
-Proof.
-intros. rewrite lt_succ. now Zle_intro1.
-Qed.
+Theorem Zle_succ_le_or_eq_succ : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
+Proof NZle_succ_le_or_eq_succ.
 
-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 Zneq_succ_l : forall n : Z, S n ~= n.
+Proof NZneq_succ_l.
 
-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 Znlt_succ_l : forall n : Z, ~ S n < n.
+Proof NZnlt_succ_l.
 
-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 Znle_succ_l : forall n : Z, ~ S n <= n.
+Proof NZnle_succ_l.
 
-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 Zlt_le_succ : forall n m : Z, n < m <-> S n <= m.
+Proof NZlt_le_succ.
 
-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 Zlt_succ_lt : forall n m : Z, S n < m -> n < m.
+Proof NZlt_succ_lt.
 
-Theorem lt_predn_m : forall n m, n < m -> P n < m.
-Proof.
-intros; rewrite lt_pred; now Zle_intro1.
-Qed.
+Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m.
+Proof NZle_succ_le.
 
-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 Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
+Proof NZsucc_lt_mono.
 
-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 Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
+Proof NZsucc_le_mono.
 
-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 Zlt_asymm : forall n m, n < m -> ~ m < n.
+Proof NZlt_asymm.
 
-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 Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
+Proof NZlt_trans.
 
-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 Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
+Proof NZle_trans.
 
-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 Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
+Proof NZle_lt_trans.
 
-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 Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
+Proof NZlt_le_trans.
 
-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 Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
+Proof NZle_antisymm.
 
-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.
+(** Trichotomy, decidability, and double negation elimination *)
 
-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 Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
+Proof NZlt_trichotomy.
 
-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 Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
+Proof NZle_gt_cases.
 
-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 Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
+Proof NZlt_ge_cases.
 
-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 Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
+Proof NZle_ngt.
 
-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 Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
+Proof NZnlt_ge.
 
-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 Zlt_em : forall n m : Z, n < m \/ ~ n < m.
+Proof NZlt_em.
 
-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 Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
+Proof NZlt_dne.
 
-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 Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
+Proof NZnle_gt.
 
-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 Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
+Proof NZlt_nge.
 
-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 Zle_em : forall n m : Z, n <= m \/ ~ n <= m.
+Proof NZle_em.
 
-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 Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
+Proof NZle_dne.
 
-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 Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n.
+Proof NZlt_nlt_succ.
 
-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 Zlt_exists_pred :
+  forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
+Proof NZlt_exists_pred.
 
-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 Zlt_succ_iter_r :
+  forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
+Proof NZlt_succ_iter_r.
 
-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 Zneq_succ_iter_l :
+  forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
+Proof NZneq_succ_iter_l.
+
+(** Stronger variant of induction with assumptions n >= 0 (n < 0)
+in the induction step *)
+
+Theorem Zright_induction :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z, A z ->
+      (forall n : Z, z <= n -> A n -> A (S n)) ->
+        forall n : Z, z <= n -> A n.
+Proof NZright_induction.
 
-Theorem lt_total : forall n m,  n < m \/ n == m \/ m < n.
+Theorem Zleft_induction :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z, A z ->
+      (forall n : Z, n < z -> A (S n) -> A n) ->
+        forall n : Z, n <= z -> A n.
+Proof NZleft_induction.
+
+Theorem Zorder_induction :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z, A z ->
+      (forall n : Z, z <= n -> A n -> A (S n)) ->
+      (forall n : Z, n < z -> A (S n) -> A n) ->
+        forall n : Z, A n.
+Proof NZorder_induction.
+
+Theorem Zorder_induction' :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z, A z ->
+      (forall n : Z, z <= n -> A n -> A (S n)) ->
+      (forall n : Z, n <= z -> A n -> A (P n)) ->
+        forall n : Z, A 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.
+intros A A_wd z Az AS AP n; apply Zorder_induction with (z := z); try assumption.
+intros m H1 H2. apply AP in H2; [| now apply -> Zlt_le_succ].
+unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
+[assumption | apply Zpred_succ].
 Qed.
 
-Theorem le_gt : forall n m, n <= m <-> ~ m < n.
+Theorem Zright_induction' :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z,
+      (forall n : Z, n <= z -> A n) ->
+      (forall n : Z, z <= n -> A n -> A (S n)) ->
+        forall n : Z, A n.
+Proof NZright_induction'.
+
+Theorem Zstrong_right_induction' :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall z : Z,
+      (forall n : Z, n <= z -> A n) ->
+      (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
+        forall n : Z, A n.
+Proof NZstrong_right_induction'.
+
+(** Elimintation principle for < *)
+
+Theorem Zlt_ind :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall n : Z,
+      A (S n) ->
+      (forall m : Z, n < m -> A m -> A (S m)) ->
+        forall m : Z, n < m -> A m.
+Proof NZlt_ind.
+
+(** Elimintation principle for <= *)
+
+Theorem Zle_ind :
+  forall A : Z -> Prop, predicate_wd E A ->
+    forall n : Z,
+      A n ->
+      (forall m : Z, n <= m -> A m -> A (S m)) ->
+        forall m : Z, n <= m -> A m.
+Proof NZle_ind.
+
+Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction with (z := 0)).
+
+(** Theorems that are either not valid on N or have different proofs on N and Z *)
+
+Theorem Zlt_pred_l : forall n : Z, P n < 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.
+intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r.
 Qed.
 
-Theorem lt_ge : forall n m, n < m <-> ~ m <= n.
+Theorem Zle_pred_l : forall n : Z, P n <= 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.
+intro; le_less; apply Zlt_pred_l.
 Qed.
 
-Theorem lt_discrete : forall n m, n < m -> m < S n -> False.
+Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
 Proof.
-intros n m H1 H2; apply -> lt_succ in H2; apply -> lt_ge in H1; false_hyp H2 H1.
+intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_le.
 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.
+Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
 Proof.
-intros n H. pose proof (lt_n_succn n) as H1. rewrite H in H1. false_hyp H1 lt_irr.
+intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl.
 Qed.
 
-Theorem neq_predn_n : forall n, P n # n.
+Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
 Proof.
-intros n H. apply succ_wd in H. rewrite succ_pred in H. now apply neq_succn_n with (n := n).
+intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
+apply Zlt_le_succ.
 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.
+Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
 Proof.
-intros n m; induction n as [| n IH]; simpl in *.
-apply lt_n_succn. now apply lt_n_succm.
+intros; apply <- Zlt_pred_le; le_less.
 Qed.
 
-Lemma lt_predkm_m :
-  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m < m.
+Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
 Proof.
-intros n m; induction n as [| n IH]; simpl in *.
-apply lt_predn_n. now apply lt_predn_m.
+intros; le_less; now apply <- Zlt_pred_le.
 Qed.
 
-Theorem neq_m_succkm :
-  forall (n : nat) (m : Z), nth_succ (Datatypes.S n) m # m.
+Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
 Proof.
-intros n m H. pose proof (lt_m_succkm n m) as H1. rewrite H in H1.
-false_hyp H1 lt_irr.
+intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l].
 Qed.
 
-Theorem neq_predkm_m :
-  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m # m.
+Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
 Proof.
-intros n m H. pose proof (lt_predkm_m n m) as H1. rewrite H in H1.
-false_hyp H1 lt_irr.
+intros; le_less; now apply <- Zlt_le_pred.
 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.
+Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
 Proof.
-intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le.
 Qed.
 
-Theorem right_induction :
-  A z -> (forall n, z <= n -> A n -> A (S n)) -> forall n, z <= n -> A n.
+Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m.
 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.
+intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred.
 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.
+Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m.
 Proof.
-intros x1 x2 H; unfold Q'; qmorphism x1 x2.
+intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ.
 Qed.
 
-Theorem left_induction :
-  A z -> (forall n, n <= z -> A n -> A (P n)) -> forall n, n <= z -> A n.
+Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m.
 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.
+intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ.
 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.
+Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
 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].
+intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_le.
 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.
+Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S 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.
+intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_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.
+Theorem Zneq_pred_l : forall n : Z, P n ~= n.
 Proof.
-intros n H1 H2 m H3.
-now apply right_induction with n.
+intro; apply Zlt_neq; apply Zlt_pred_l.
 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.
-
-
+End ZOrderPropFunct.
 
-(*
- 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
index 624f85f04..c22b346b4 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -1,228 +1,218 @@
-Require Export ZAxioms.
+Require Export ZBase.
 
-Module Type ZPlusSignature.
-Declare Module Export ZBaseMod : ZBaseSig.
-Open Local Scope IntScope.
+Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
+Open Local Scope NatIntScope.
 
-Parameter Inline plus : Z -> Z -> Z.
-Parameter Inline minus : Z -> Z -> Z.
-Parameter Inline uminus : Z -> Z.
+Theorem Zplus_0_l : forall n : Z, 0 + n == n.
+Proof NZplus_0_l.
 
-Notation "x + y" := (plus x y) : IntScope.
-Notation "x - y" := (minus x y) : IntScope.
-Notation "- x" := (uminus x) : IntScope.
+Theorem Zplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
+Proof NZplus_succ_l.
 
-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.
+Theorem Zminus_0_r : forall n : Z, n - 0 == n.
+Proof NZminus_0_r.
 
-Axiom plus_0 : forall n, 0 + n == n.
-Axiom plus_succ : forall n m, (S n) + m == S (n + m).
+Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Proof NZminus_succ_r.
 
-Axiom minus_0 : forall n, n - 0 == n.
-Axiom minus_succ : forall n m, n - (S m) == P (n - m).
+Theorem Zopp_0 : - 0 == 0.
+Proof Zopp_0.
 
-Axiom uminus_0 : - 0 == 0.
-Axiom uminus_succ : forall n, - (S n) == P (- n).
+Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
+Proof Zopp_succ.
 
-End ZPlusSignature.
+(** Theorems that are valid for both natural numbers and integers *)
 
-Module ZPlusProperties (Import ZPlusModule : ZPlusSignature).
-Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
-Open Local Scope IntScope.
+Theorem Zplus_0_r : forall n : Z, n + 0 == n.
+Proof NZplus_0_r.
 
-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 Zplus_succ_r : forall n m : Z, n + S m == S (n + m).
+Proof NZplus_succ_r.
 
-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 Zplus_comm : forall n m : Z, n + m == m + n.
+Proof NZplus_comm.
 
-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 Zplus_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
+Proof NZplus_assoc.
+
+Theorem Zplus_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
+Proof NZplus_shuffle1.
 
-Theorem plus_n_0 : forall n, n + 0 == n.
+Theorem Zplus_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
+Proof NZplus_shuffle2.
+
+Theorem Zplus_1_l : forall n : Z, 1 + n == S n.
+Proof NZplus_1_l.
+
+Theorem Zplus_1_r : forall n : Z, n + 1 == S n.
+Proof NZplus_1_r.
+
+Theorem Zplus_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
+Proof NZplus_cancel_l.
+
+Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
+Proof NZplus_cancel_r.
+
+(** Theorems that are either not valid on N or have different proofs on N and Z *)
+
+Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m).
 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.
+intros n m.
+pattern n at 2. qsetoid_rewrite <- (Zsucc_pred n).
+rewrite Zplus_succ_l. now rewrite Zpred_succ.
 Qed.
 
-Theorem plus_n_succm : forall n m, n + S m == S (n + m).
+Theorem Zplus_pred_r : forall n m : Z, n + P m == P (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.
+intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m);
+apply Zplus_pred_l.
 Qed.
 
-Theorem plus_n_predm : forall n m, n + P m == P (n + m).
+Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m.
 Proof.
-intros n m; rewrite_succ_pred m at 2. rewrite plus_n_succm; now rewrite pred_succ.
+NZinduct m.
+rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r.
+intro m. rewrite Zopp_succ, Zminus_succ_r, Zplus_pred_r; now rewrite Zpred_inj_wd.
 Qed.
 
-Theorem plus_opp_minus : forall n m, n + (- m) == n - m.
+Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
 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.
+intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l.
 Qed.
 
-Theorem minus_0_n : forall n, 0 - n == - n.
+Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m).
 Proof.
-intro n; rewrite <- plus_opp_minus; now rewrite plus_0.
+intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l.
 Qed.
 
-Theorem minus_succn_m : forall n m, S n - m == S (n - m).
+Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m).
 Proof.
-intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_succ.
+intros n m. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
+rewrite Zminus_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem minus_predn_m : forall n m, P n - m == P (n - m).
+Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m).
 Proof.
-intros n m. rewrite_succ_pred n at 2; rewrite minus_succn_m; now rewrite pred_succ.
+intros n m. pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m).
+rewrite Zminus_succ_r; now rewrite Zsucc_pred.
 Qed.
 
-Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
+Theorem Zopp_pred : forall n : Z, - (P n) == S (- n).
 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.
+intro n. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
+rewrite Zopp_succ. now rewrite Zsucc_pred.
 Qed.
 
-Theorem plus_comm : forall n m, n + m == m + n.
+Theorem Zminus_diag : forall n : Z, n - n == 0.
 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.
+NZinduct n.
+now rewrite Zminus_0_r.
+intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem minus_diag : forall n, n - n == 0.
+Theorem Zplus_opp_r : forall n : Z, 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.
+intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag.
 Qed.
 
-Theorem plus_opp_r : forall n, n + (- n) == 0.
+Theorem Zplus_opp_l : forall n : Z, - n + n == 0.
 Proof.
-intro n; rewrite plus_opp_minus; now rewrite minus_diag.
+intro n; rewrite Zplus_comm; apply Zplus_opp_r.
 Qed.
 
-Theorem plus_opp_l : forall n, - n + n == 0.
+Theorem Zminus_swap : forall n m : Z, - m + n == n - m.
 Proof.
-intro n; rewrite plus_comm; apply plus_opp_r.
+intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm.
 Qed.
 
-Theorem minus_swap : forall n m, - m + n == n - m.
+Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
 Proof.
-intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm.
+intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc.
 Qed.
 
-Theorem plus_minus_inverse : forall n m, n + (m - n) == m.
+Theorem Zopp_involutive : forall n : Z, - (- n) == n.
 Proof.
-intros n m; rewrite <- minus_swap. rewrite plus_assoc;
-rewrite plus_opp_r; now rewrite plus_0.
+NZinduct n.
+now do 2 rewrite Zopp_0.
+intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd.
 Qed.
 
-Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p.
+Theorem Zopp_plus_distr : forall n m : Z, - (n + m) == - n + (- m).
 Proof.
-intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc.
+intros n m; NZinduct n.
+rewrite Zopp_0; now do 2 rewrite Zplus_0_l.
+intro n. rewrite Zplus_succ_l; do 2 rewrite Zopp_succ; rewrite Zplus_pred_l.
+now rewrite Zpred_inj_wd.
 Qed.
 
-Theorem double_opp : forall n, - (- n) == n.
+Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m.
 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.
+intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr.
+now rewrite Zopp_involutive.
 Qed.
 
-Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m).
+Theorem Zopp_inj : forall n m : Z, - 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.
+intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H.
 Qed.
 
-Theorem opp_minus_distr : forall n m, - (n - m) == - n + m.
+Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m.
 Proof.
-intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr.
-now rewrite double_opp.
+intros n m; split; [apply Zopp_inj | apply Zopp_wd].
 Qed.
 
-Theorem opp_inj : forall n m, - n == - m -> n == m.
+Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
 Proof.
-intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H.
+intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc.
+now do 2 rewrite Zplus_opp_minus.
 Qed.
 
-Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p.
+Theorem Zminus_minus_distr : forall n m p : Z, 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.
+intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc.
+now rewrite Zplus_opp_minus.
 Qed.
 
-Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p.
+Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m.
 Proof.
-intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc.
-now rewrite plus_opp_minus.
+intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive.
 Qed.
 
-Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m.
+Theorem Zplus_minus_swap : forall n m p : Z, 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.
+intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc.
+now rewrite Zminus_swap.
 Qed.
 
-Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p.
+Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n.
 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.
+intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc;
+rewrite Zminus_diag; now rewrite Zplus_0_r.
 Qed.
 
-Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p.
+Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n.
 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.
+intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r.
 Qed.
 
-Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m.
+Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p.
 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.
+intros n m p.
+stepl (-m + (m + p) == -m + n) by apply Zplus_cancel_l.
+stepr (p == n - m) by now split.
+rewrite Zplus_assoc, Zplus_opp_l, Zplus_0_l. now rewrite Zminus_swap.
 Qed.
 
-Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p.
+Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m.
 Proof.
-intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H.
+intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l.
 Qed.
 
-Lemma minus_eq : forall n m, n - m == 0 -> n == m.
+Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m.
 Proof.
-intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
+intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split.
 Qed.
 
-End ZPlusProperties.
-
+End ZPlusPropFunct.
 
-(*
- 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
index 95f0fa8c6..bab1bb4a0 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -1,167 +1,365 @@
 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.
+Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
+Open Local Scope NatIntScope.
 
-Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
+(** Theorems that are true on both natural numbers and integers *)
+
+Theorem Zplus_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
+Proof NZplus_lt_mono_l.
+
+Theorem Zplus_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p.
+Proof NZplus_lt_mono_r.
+
+Theorem Zplus_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q.
+Proof NZplus_lt_mono.
+
+Theorem Zplus_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m.
+Proof NZplus_le_mono_l.
+
+Theorem Zplus_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p.
+Proof NZplus_le_mono_r.
+
+Theorem Zplus_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q.
+Proof NZplus_le_mono.
+
+Theorem Zplus_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q.
+Proof NZplus_lt_le_mono.
+
+Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
+Proof NZplus_le_lt_mono.
+
+Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
+Proof NZle_lt_plus_lt.
+
+Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
+Proof NZlt_le_plus_lt.
+
+Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_lt.
+
+Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
+Proof NZplus_lt_cases.
+
+Theorem Zplus_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q.
+Proof NZplus_le_cases.
+
+Theorem Zplus_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0.
+Proof NZplus_neg_cases.
+
+Theorem Zplus_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m.
+Proof NZplus_pos_cases.
+
+Theorem Zplus_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0.
+Proof NZplus_nonpos_cases.
+
+Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
+Proof NZplus_nonneg_cases.
+
+(** Multiplication and order *)
+
+Theorem Ztimes_lt_pred :
+  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Proof NZtimes_lt_pred.
+
+Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZtimes_lt_mono_pos_l.
+
+Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZtimes_lt_mono_pos_r.
+
+Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
+Proof NZtimes_lt_mono_neg_l.
+
+Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
+Proof NZtimes_lt_mono_neg_r.
+
+Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
+Proof NZtimes_le_mono_nonneg_l.
+
+Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
+Proof NZtimes_le_mono_nonpos_l.
+
+Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
+Proof NZtimes_le_mono_nonneg_r.
+
+Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
+Proof NZtimes_le_mono_nonpos_r.
+
+Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZtimes_cancel_l.
+
+Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZtimes_le_mono_pos_l.
+
+Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZtimes_le_mono_pos_r.
+
+Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
+Proof NZtimes_le_mono_neg_l.
+
+Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
+Proof NZtimes_le_mono_neg_r.
+
+Theorem Ztimes_lt_mono :
+  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
+Proof NZtimes_lt_mono.
+
+Theorem Ztimes_le_mono :
+  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
+Proof NZtimes_le_mono.
+
+Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZtimes_pos_pos.
+
+Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
+Proof NZtimes_nonneg_nonneg.
+
+Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
+Proof NZtimes_neg_neg.
+
+Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
+Proof NZtimes_nonpos_nonpos.
+
+Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
+Proof NZtimes_pos_neg.
+
+Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
+Proof NZtimes_nonneg_nonpos.
+
+Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
+Proof NZtimes_neg_pos.
+
+Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
+Proof NZtimes_nonpos_nonneg.
+
+Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
+Proof NZtimes_eq_0.
+
+Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZtimes_neq_0.
+
+(** Theorems that are either not valid on N or have different proofs on N and Z *)
+
+(** Minus and order *)
+
+Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n.
+Proof.
+intros n m. stepr (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_plus_diag.
+Qed.
+
+Theorem Zle_le_minus : forall n m : Z, n <= m <-> 0 <= m - n.
+Proof.
+intros n m; stepr (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_plus_diag.
+Qed.
+
+Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n.
+Proof.
+intros n m. stepr (m + - m < m + - n) by symmetry; apply Zplus_lt_mono_l.
+do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zlt_lt_minus.
+Qed.
+
+Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.
+Proof.
+intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zplus_le_mono_l.
+do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zle_le_minus.
+Qed.
+
+Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
+Proof.
+intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0.
+Qed.
+
+Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n.
+Proof.
+intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0.
+Qed.
+
+Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0.
+Proof.
+intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0.
+Qed.
+
+Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n.
+Proof.
+intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0.
+Qed.
+
+Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.
+Proof.
+intros n m p. do 2 rewrite <- Zplus_opp_minus. rewrite <- Zplus_lt_mono_l.
+apply Zopp_lt_mono.
+Qed.
+
+Theorem Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p.
+Proof.
+intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_lt_mono_r.
+Qed.
+
+Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_trans with (m - p);
+[now apply -> Zminus_lt_mono_r | now apply -> Zminus_lt_mono_l].
+Qed.
+
+Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.
+Proof.
+intros n m p; do 2 rewrite <- Zplus_opp_minus; rewrite <- Zplus_le_mono_l;
+apply Zopp_le_mono.
+Qed.
+
+Theorem Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p.
+Proof.
+intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_le_mono_r.
+Qed.
+
+Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.
+Proof.
+intros n m p q H1 H2.
+apply NZle_trans with (m - p);
+[now apply -> Zminus_le_mono_r | now apply -> Zminus_le_mono_l].
+Qed.
+
+Theorem Zminus_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q.
+Proof.
+intros n m p q H1 H2.
+apply NZlt_le_trans with (m - p);
+[now apply -> Zminus_lt_mono_r | now apply -> Zminus_le_mono_l].
+Qed.
+
+Theorem Zminus_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q.
 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.
+intros n m p q H1 H2.
+apply NZle_lt_trans with (m - p);
+[now apply -> Zminus_le_mono_r | now apply -> Zminus_lt_mono_l].
 Qed.
 
-Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p.
+Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.
 Proof.
-intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
-apply plus_lt_compat_l.
+intros n m p q H1 H2. apply (Zle_lt_plus_lt (- m) (- n));
+[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
-Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m.
+Theorem Zlt_le_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.
 Proof.
-intros n m p; do 2 rewrite <- lt_succ. rewrite <- plus_n_succm;
-apply plus_lt_compat_l.
+intros n m p q H1 H2. apply (Zlt_le_plus_lt (- m) (- n));
+[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
-Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p.
+Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
-intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p);
-apply plus_le_compat_l.
+intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n));
+[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
-Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Theorem Zlt_plus_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p.
 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.
+intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r.
+now rewrite Zplus_minus_diag.
 Qed.
 
-Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Theorem Zle_plus_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p.
 Proof.
-intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat.
-rewrite H2. now apply -> plus_lt_compat_r.
+intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r.
+now rewrite Zplus_minus_diag.
 Qed.
 
-Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Theorem Zlt_plus_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n.
 Proof.
-intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat.
-rewrite H1. now apply -> plus_lt_compat_l.
+intros n m p. rewrite Zplus_comm; apply Zlt_plus_lt_minus_r.
 Qed.
 
-Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Theorem Zle_plus_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n.
 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.
+intros n m p. rewrite Zplus_comm; apply Zle_plus_le_minus_r.
 Qed.
 
-Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.
+Theorem Zlt_minus_lt_plus_r : forall n m p : Z, n - p < m <-> n < m + p.
 Proof.
-intros; rewrite <- (plus_0 0); now apply plus_le_compat.
+intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zplus_lt_mono_r.
+now rewrite Zminus_plus_diag.
 Qed.
 
-Lemma lt_opp_forward : forall n m, n < m -> - m < - n.
+Theorem Zle_minus_le_plus_r : forall n m p : Z, n - p <= m <-> n <= m + p.
 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.
+intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zplus_le_mono_r.
+now rewrite Zminus_plus_diag.
 Qed.
 
-Theorem lt_opp : forall n m, n < m <-> - m < - n.
+Theorem Zlt_minus_lt_plus_l : forall n m p : Z, n - m < p <-> n < m + p.
 Proof.
-intros n m; split.
-apply lt_opp_forward.
-intro; rewrite <- (double_opp n); rewrite <- (double_opp m);
-now apply lt_opp_forward.
+intros n m p. rewrite Zplus_comm; apply Zlt_minus_lt_plus_r.
 Qed.
 
-Theorem le_opp : forall n m, n <= m <-> - m <= - n.
+Theorem Zle_minus_le_plus_l : forall n m p : Z, n - m <= p <-> n <= m + p.
 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.
+intros n m p. rewrite Zplus_comm; apply Zle_minus_le_plus_r.
 Qed.
 
-Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n.
+Theorem Zlt_minus_lt_plus : forall n m p q : Z, n - m < p - q <-> n + q < m + p.
 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.
+intros n m p q. rewrite Zlt_minus_lt_plus_l. rewrite Zplus_minus_assoc.
+now rewrite <- Zlt_plus_lt_minus_r.
 Qed.
 
-Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n.
+Theorem Zle_minus_le_plus : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.
 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.
+intros n m p q. rewrite Zle_minus_le_plus_l. rewrite Zplus_minus_assoc.
+now rewrite <- Zle_plus_le_minus_r.
 Qed.
 
-Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0.
+Theorem Zlt_minus_pos : forall n m : Z, 0 < m <-> n - m < 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.
+intros n m. stepr (n - m < n - 0) by now rewrite Zminus_0_r. apply Zminus_lt_mono_l.
 Qed.
 
-Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0.
+Theorem Zle_minus_nonneg : forall n m : Z, 0 <= m <-> n - m <= 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.
+intros n m. stepr (n - m <= n - 0) by now rewrite Zminus_0_r. apply Zminus_le_mono_l.
 Qed.
 
-Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n.
+Theorem Zminus_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p.
 Proof.
-intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l.
-apply lt_opp.
+intros n m p q H. rewrite Zlt_minus_lt_plus in H. now apply Zplus_lt_cases.
 Qed.
 
-Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n.
+Theorem Zminus_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p.
 Proof.
-intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l.
-apply le_opp.
+intros n m p q H. rewrite Zle_minus_le_plus in H. now apply Zplus_le_cases.
 Qed.
 
-Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p.
+Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
-intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r.
+intros n m H; rewrite <- Zplus_opp_minus in H.
+setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos).
+now apply Zplus_neg_cases.
 Qed.
 
-Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p.
+Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r.
+intros n m H; rewrite <- Zplus_opp_minus in H.
+setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg).
+now apply Zplus_pos_cases.
 Qed.
 
-Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p.
+Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
 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.
+intros n m H; rewrite <- Zplus_opp_minus in H.
+setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg).
+now apply Zplus_nonpos_cases.
 Qed.
 
-Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p.
+Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
 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.
+intros n m H; rewrite <- Zplus_opp_minus in H.
+setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos).
+now apply Zplus_nonneg_cases.
 Qed.
 
-End ZPlusOrderProperties.
+End ZPlusOrderPropFunct.
 
 
-(*
- 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
index ffcb2dea8..4814ab086 100644
--- a/theories/Numbers/Integer/Abstract/ZPred.v
+++ b/theories/Numbers/Integer/Abstract/ZPred.v
@@ -52,9 +52,3 @@ rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))
 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
index 38311aa2b..bc7321cba 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -1,127 +1,108 @@
+Require Export Ring.
 Require Export ZPlus.
 
-Module Type ZTimesSignature.
-Declare Module Export ZPlusModule : ZPlusSignature.
-Open Local Scope IntScope.
+Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
+Open Local Scope NatIntScope.
 
-Parameter Inline times : Z -> Z -> Z.
+Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
+Proof NZtimes_0_r.
 
-Notation "x * y" := (times x y) : IntScope.
+Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Proof NZtimes_succ_r.
 
-Add Morphism times with signature E ==> E ==> E as times_wd.
+(** Theorems that are valid for both natural numbers and integers *)
 
-Axiom times_0 : forall n, n * 0 == 0.
-Axiom times_succ : forall n m, n * (S m) == n * m + n.
+Theorem Ztimes_0_l : forall n : Z, 0 * n == 0.
+Proof NZtimes_0_l.
 
-End ZTimesSignature.
+Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
+Proof NZtimes_succ_l.
 
-Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
-Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
-Open Local Scope IntScope.
+Theorem Ztimes_comm : forall n m : Z, n * m == m * n.
+Proof NZtimes_comm.
 
-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 Ztimes_plus_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
+Proof NZtimes_plus_distr_r.
 
-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 Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
+Proof NZtimes_plus_distr_l.
 
-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 Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
+Proof NZtimes_assoc.
 
-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 Ztimes_1_l : forall n : Z, 1 * n == n.
+Proof NZtimes_1_l.
 
-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 Ztimes_1_r : forall n : Z, n * 1 == n.
+Proof NZtimes_1_r.
+
+(* The following two theorems are true in an ordered ring,
+but since they don't mention order, we'll put them here *)
+
+Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
+Proof NZtimes_eq_0.
 
-Theorem times_opp_r : forall n m, n * (- m) == - (n * m).
+Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZtimes_neq_0.
+
+(** Z forms a ring *)
+
+Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZE.
 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.
+constructor.
+exact Zplus_0_l.
+exact Zplus_comm.
+exact Zplus_assoc.
+exact Ztimes_1_l.
+exact Ztimes_comm.
+exact Ztimes_assoc.
+exact Ztimes_plus_distr_r.
+intros; now rewrite Zplus_opp_minus.
+exact Zplus_opp_r.
 Qed.
 
-Theorem times_opp_l : forall n m, (- n) * m == - (n * m).
+Add Ring ZR : Zring.
+
+(** Theorems that are either not valid on N or have different proofs on N and Z *)
+
+Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n.
 Proof.
-intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m);
-now rewrite times_opp_r.
+intros n m.
+pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m).
+now rewrite Ztimes_succ_r, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
 Qed.
 
-Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m.
+Theorem Ztimes_pred_l : forall n m : Z, (P n) * m == n * m - m.
 Proof.
-intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp.
+intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r.
 Qed.
 
-Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p.
+Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m).
 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.
+intros; ring.
 Qed.
 
-Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p.
+Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m).
 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).
+intros; ring.
 Qed.
 
-Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p.
+Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
 Proof.
-intros n m p.
-do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r.
+intros; ring.
 Qed.
 
-Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p.
+Theorem Ztimes_minus_distr_r : forall n m p : Z, n * (m - p) == n * m - n * p.
 Proof.
-intros n m p.
-do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l.
+intros; ring.
 Qed.
 
-Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
+Theorem Ztimes_minus_distr_l : forall n m p : Z, (n - m) * p == n * p - 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.
+intros; ring.
 Qed.
 
-End ZTimesProperties.
+End ZTimesPropFunct.
 
 
-(*
- 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
index 055342bcc..d63dc0d8c 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -1,96 +1,102 @@
-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:
-*)
+Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
+Open Local Scope NatIntScope.
+
+(** Theorems that are true on both natural numbers and integers *)
+
+Theorem Ztimes_lt_pred :
+  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Proof NZtimes_lt_pred.
+
+Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZtimes_lt_mono_pos_l.
+
+Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZtimes_lt_mono_pos_r.
+
+Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
+Proof NZtimes_lt_mono_neg_l.
+
+Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
+Proof NZtimes_lt_mono_neg_r.
+
+Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
+Proof NZtimes_le_mono_nonneg_l.
+
+Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
+Proof NZtimes_le_mono_nonpos_l.
+
+Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
+Proof NZtimes_le_mono_nonneg_r.
+
+Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
+Proof NZtimes_le_mono_nonpos_r.
+
+Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZtimes_cancel_l.
+
+Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZtimes_le_mono_pos_l.
+
+Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZtimes_le_mono_pos_r.
+
+Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
+Proof NZtimes_le_mono_neg_l.
+
+Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
+Proof NZtimes_le_mono_neg_r.
+
+Theorem Ztimes_lt_mono :
+  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
+Proof NZtimes_lt_mono.
+
+Theorem Ztimes_le_mono :
+  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
+Proof NZtimes_le_mono.
+
+Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZtimes_pos_pos.
+
+Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
+Proof NZtimes_nonneg_nonneg.
+
+Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
+Proof NZtimes_neg_neg.
+
+Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
+Proof NZtimes_nonpos_nonpos.
+
+Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
+Proof NZtimes_pos_neg.
+
+Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
+Proof NZtimes_nonneg_nonpos.
+
+Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
+Proof NZtimes_neg_pos.
+
+Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
+Proof NZtimes_nonpos_nonneg.
+
+Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
+Proof NZtimes_eq_0.
+
+Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZtimes_neq_0.
+
+Theorem Ztimes_pos : forall n m : Z, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
+Proof NZtimes_pos.
+
+Theorem Ztimes_neg :
+  forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
+Proof NZtimes_neg.
+
+(** Theorems that are either not valid on N or have different proofs on N and Z *)
+
+(* None? *)
+
+End ZTimesOrderPropFunct.
+
diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v
index f5c19c611..a1e52a202 100644
--- a/theories/Numbers/Integer/BigInts/EZBase.v
+++ b/theories/Numbers/Integer/BigInts/EZBase.v
@@ -159,9 +159,3 @@ Qed.
 End Induction.
 
 End EZBaseMod.
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v
index ca3286211..b31dcdf9d 100644
--- a/theories/Numbers/Integer/BigInts/Zeqmod.v
+++ b/theories/Numbers/Integer/BigInts/Zeqmod.v
@@ -40,9 +40,3 @@ Theorem Zplus_eqmod_compat_r :
 intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k);
 apply Zplus_eqmod_compat_l.
 Qed.
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 217d08850..0fd1be7a9 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -197,8 +197,3 @@ End ZBinOrder.
 Module Export ZTimesOrderPropertiesModule :=
   ZTimesOrderProperties ZBinTimes ZBinOrder.
 
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index 73b0bee7e..2a9b4f386 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -140,9 +140,3 @@ End Induction.
 
 End NatPairsInt.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
index 8943afde9..dc258f873 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
@@ -110,9 +110,3 @@ End NatPairsPlusOrderProperties.*)
 NatPairsOrderModule.ZBaseMod are the same *)
 
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
index d1ae7679b..2e658c181 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
@@ -81,9 +81,3 @@ Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
 Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
 End NatPairsPlusProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
index 47bf8cd08..553c6df22 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
@@ -54,9 +54,3 @@ Module Export NatPairsTimesModule := NatPairsTimes NTimesMod.
 Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
 End NatPairsTimesProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 0a89132ea..1509b5f7d 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -72,9 +72,3 @@ 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
index fbccf049c..121f78813 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -74,9 +74,3 @@ Tactic Notation "NZinduct" ident(n) constr(u) :=
 
 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
deleted file mode 100644
index f35e030e1..000000000
--- a/theories/Numbers/NatInt/NZOrdRing.v
+++ /dev/null
@@ -1,26 +0,0 @@
-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
deleted file mode 100644
index fd7cf608a..000000000
--- a/theories/Numbers/NatInt/NZOrder.g
+++ /dev/null
@@ -1,219 +0,0 @@
-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
index f5b757a20..5c6369fe4 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -127,7 +127,7 @@ 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.
+Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
 Proof.
 intros n m; NZinduct n m.
 intros H _; false_hyp H NZlt_irrefl.
@@ -138,11 +138,6 @@ 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.
@@ -151,8 +146,8 @@ 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).
+le_elim H3. assumption. rewrite <- H3 in H2.
+elimtype False; now apply (NZlt_asymm n m).
 Qed.
 
 Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
@@ -177,7 +172,7 @@ 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) | | |].
+[elimtype False; apply (NZlt_asymm n m) | | |].
 Qed.
 
 (** Trichotomy, decidability, and double negation elimination *)
@@ -187,12 +182,18 @@ 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).
+rewrite <- (NZle_lt_or_eq (S n) m).
+setoid_replace (n == m) with (m == n) using relation iff by now split.
 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.
+(* Decidability of equality, even though true in each finite ring, does not
+have a uniform proof. Otherwise, the proof for two fixed numbers would
+reduce to a normal form that will say if the numbers are equal or not,
+which cannot be true in all finite rings. Therefore, we prove decidability
+in the presence of order. *)
+Theorem NZeq_em : 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.
@@ -200,69 +201,88 @@ 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.
+Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
-destruct (NZE_dec n m) as [H1 | H1].
+destruct (NZeq_em 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.
+Theorem NZneq_lt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m.
 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.
+Theorem NZle_gt_cases : forall n m : NZ, n <= m \/ n > m.
 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.
+(* The following theorem is cleary redundant, but helps not to
+remember whether one has to say le_gt_cases or lt_ge_cases *)
+Theorem NZlt_ge_cases : forall n m : NZ, n < m \/ n >= m.
+Proof.
+intros n m; destruct (NZle_gt_cases m n); try (now left); try (now right).
+Qed.
+
+Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m.
 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].
+destruct (NZle_gt_cases n m) as [H1 | H1].
 assumption. false_hyp H1 H.
 Qed.
 
-Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m.
+(* Redundant but useful *)
+Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m.
+Proof.
+intros n m; symmetry; apply NZle_ngt.
+Qed.
+
+Theorem NZlt_em : 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].
+intros n m; destruct (NZle_gt_cases m n);
+[right; now apply -> NZle_ngt | 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] |
+[destruct (NZlt_em 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.
+Theorem NZnle_gt : forall n m : NZ, ~ n <= m <-> n > m.
+Proof.
+intros n m. rewrite NZle_ngt. apply NZlt_dne.
+Qed.
+
+(* Redundant but useful *)
+Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m.
 Proof.
-intros n m. rewrite NZle_nlt. apply NZlt_dne.
+intros n m; symmetry; apply NZnle_gt.
 Qed.
 
-Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m.
+Theorem NZle_em : 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].
+intros n m; destruct (NZle_gt_cases n m);
+[now left | right; now apply <- NZnle_gt].
 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] |
+[destruct (NZle_em 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.
+intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_gt.
 Qed.
 
 (* The difference between integers and natural numbers is that for
@@ -276,7 +296,7 @@ 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.
+intros m H1 H2; apply <- NZnle_gt 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].
@@ -354,7 +374,7 @@ Qed.
 
 Lemma NZrbase : A' z.
 Proof.
-intros m H1 H2. apply -> NZle_nlt in H1. false_hyp H2 H1.
+intros m H1 H2. apply -> NZle_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n.
@@ -401,7 +421,7 @@ 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.
+apply -> NZle_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n.
@@ -523,7 +543,7 @@ 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.
+apply <- NZnle_gt in H2. elim H2. now apply NZle_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
@@ -531,8 +551,3 @@ End WF.
 
 End NZOrderPropFunct.
 
-(*
- 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
index 061ab84bb..4380cb1b6 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -77,9 +77,3 @@ 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
index f43b549e2..6368fa557 100644
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ b/theories/Numbers/NatInt/NZPlusOrder.v
@@ -65,9 +65,3 @@ 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
deleted file mode 100644
index 2425224b8..000000000
--- a/theories/Numbers/NatInt/NZRing.v
+++ /dev/null
@@ -1,45 +0,0 @@
-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
index ca78ced69..517a8b7ff 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -66,9 +66,3 @@ 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
index 95275f8c0..6f702067d 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -61,31 +61,64 @@ 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.
+Theorem NZle_lt_plus_lt : 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.
+intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
+pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt 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.
+Theorem NZlt_le_plus_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q.
+Proof.
+intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
+pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
+false_hyp H2 H3.
+Qed.
+
+Theorem NZle_le_plus_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
+Proof.
+intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |].
+pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
+false_hyp H2 H3.
+Qed.
+
+Theorem NZplus_lt_cases : 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.
+destruct (NZle_gt_cases p n) as [H1 | H1].
+destruct (NZle_gt_cases q m) as [H2 | H2].
+pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt 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.
+Theorem NZplus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Proof.
+intros n m p q H.
+destruct (NZle_gt_cases n p) as [H1 | H1]. now left.
+destruct (NZle_gt_cases m q) as [H2 | H2]. now right.
+assert (H3 : p + q < n + m) by now apply NZplus_lt_mono.
+apply -> NZle_ngt in H. false_hyp H3 H.
+Qed.
+
+Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
+Proof.
+intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
+Qed.
+
+Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Proof.
+intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
+Qed.
+
+Theorem NZplus_nonpos_cases : 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.
+intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
 Qed.
 
-Theorem NZplus_gt_inv_0 : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem NZplus_nonneg_cases : 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.
+intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
 Qed.
 
 (** Multiplication and order *)
@@ -107,7 +140,7 @@ 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 <- NZle_ngt 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.
@@ -124,13 +157,13 @@ Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p
 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 H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_gt 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).
+intros n1 m1 H2. apply (NZle_lt_plus_lt 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 <- NZle_ngt 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 |].
@@ -175,13 +208,13 @@ Theorem NZtimes_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n ==
 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].
+apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases 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].
+apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases 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 |].
@@ -306,10 +339,35 @@ 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.
+Theorem NZtimes_pos : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
+Proof.
+intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
+destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
+[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |];
+(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
+[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]);
+try (left; now split); try (right; now split).
+assert (H3 : n * m < 0) by now apply NZtimes_neg_pos.
+elimtype False; now apply (NZlt_asymm (n * m) 0).
+assert (H3 : n * m < 0) by now apply NZtimes_pos_neg.
+elimtype False; now apply (NZlt_asymm (n * m) 0).
+now apply NZtimes_pos_pos. now apply NZtimes_neg_neg.
+Qed.
 
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
+Theorem NZtimes_neg :
+  forall n m : NZ, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
+Proof.
+intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
+destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
+[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |];
+(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
+[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]);
+try (left; now split); try (right; now split).
+assert (H3 : n * m > 0) by now apply NZtimes_neg_neg.
+elimtype False; now apply (NZlt_asymm (n * m) 0).
+assert (H3 : n * m > 0) by now apply NZtimes_pos_pos.
+elimtype False; now apply (NZlt_asymm (n * m) 0).
+now apply NZtimes_neg_pos. now apply NZtimes_pos_neg.
+Qed.
+
+End NZTimesOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index a30c81682..444175c14 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -31,9 +31,3 @@ Axiom recursion_succ :
 
 End NAxiomsSig.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index b999240fb..9705d05ba 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -37,6 +37,12 @@ Proof NZsucc_inj_wd.
 Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
+(* Decidability of equality was proved only in NZOrder, but since it
+does not mention order, we'll put it here *)
+
+Theorem eq_em : forall n m : N, n == m \/ n ~= m.
+Proof NZeq_em.
+
 (* Now we prove that the successor of a number is not zero by defining a
 function (by recursion) that maps 0 to false and the successor to true *)
 
@@ -241,9 +247,3 @@ Ltac double_induct n m :=
 
 End NBasePropFunct.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NDepRec.v b/theories/Numbers/Natural/Abstract/NDepRec.v
index 9ad0b4650..648786854 100644
--- a/theories/Numbers/Natural/Abstract/NDepRec.v
+++ b/theories/Numbers/Natural/Abstract/NDepRec.v
@@ -70,9 +70,3 @@ Qed.
 
 End NDepRecTimesProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NDomain.v b/theories/Numbers/Natural/Abstract/NDomain.v
index a95c94ca0..8f326ffec 100644
--- a/theories/Numbers/Natural/Abstract/NDomain.v
+++ b/theories/Numbers/Natural/Abstract/NDomain.v
@@ -100,9 +100,3 @@ Ltac stepr_ring t := stepr t; [| ring].
 
 End NDomainProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 9ee79022e..66e028abe 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -110,9 +110,3 @@ Qed.
 
 End Isomorphism.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 811126123..07fc67499 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -70,13 +70,18 @@ intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
 rewrite plus_comm. apply plus_minus.
 Qed.
 
-Theorem plus_minus_eq : forall n m p : N, m + p == n -> n - m == p.
+Theorem plus_minus_eq_l : forall n m p : N, m + p == n -> n - m == p.
 Proof.
 intros n m p H. symmetry.
-assert (H1 : m + p - m == n - m). now rewrite H.
+assert (H1 : m + p - m == n - m) by now rewrite H.
 rewrite plus_comm in H1. now rewrite plus_minus in H1.
 Qed.
 
+Theorem plus_minus_eq_r : forall n m p : N, m + p == n -> n - p == m.
+Proof.
+intros n m p H; rewrite plus_comm in H; now apply plus_minus_eq_l.
+Qed.
+
 (* This could be proved by adding m to both sides. Then the proof would
 use plus_minus_assoc and le_minus_0, which is proven below. *)
 Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
@@ -137,7 +142,7 @@ Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
 Proof.
 intros n m p; induct n.
 now rewrite minus_0_l, times_0_l, minus_0_l.
-intros n IH. destruct (le_lt_dec m n) as [H | H].
+intros n IH. destruct (le_gt_cases m n) as [H | H].
 rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
 rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
 rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
@@ -156,9 +161,3 @@ Qed.
 
 End NMinusPropFunct.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v
index 362dc0516..4333d9e46 100644
--- a/theories/Numbers/Natural/Abstract/NMiscFunct.v
+++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v
@@ -396,9 +396,3 @@ Module Export DefaultTimesOrderProperties :=
 
 End MiscFunctFunctor.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index e8311c63c..f62b5ecb2 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -8,17 +8,17 @@ Open Local Scope NatIntScope.
 
 (* Axioms *)
 
-Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
+Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m.
 Proof NZle_lt_or_eq.
 
-Theorem lt_succ_le : forall x y, x < S y <-> x <= y.
+Theorem lt_irrefl : forall n : N, ~ n < n.
+Proof NZlt_irrefl.
+
+Theorem lt_succ_le : forall n m : N, n < S m <-> n <= m.
 Proof NZlt_succ_le.
 
 (* Renaming theorems from NZOrder.v *)
 
-Theorem lt_irrefl : forall n : N, ~ (n < n).
-Proof NZOrdAxiomsMod.NZlt_irrefl.
-
 Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
 Proof NZlt_le_incl.
 
@@ -67,9 +67,6 @@ Proof NZsucc_lt_mono.
 Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m.
 Proof NZsucc_le_mono.
 
-Theorem lt_lt_false : forall n m, n < m -> m < n -> False.
-Proof NZlt_lt_false.
-
 Theorem lt_asymm : forall n m, n < m -> ~ m < n.
 Proof NZlt_asymm.
 
@@ -93,23 +90,32 @@ Proof NZle_antisymm.
 Theorem lt_trichotomy : forall n m : N,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
-Theorem le_lt_dec : forall n m : N, n <= m \/ m < n.
-Proof NZle_lt_dec.
+Theorem le_gt_cases : forall n m : N, n <= m \/ n > m.
+Proof NZle_gt_cases.
+
+Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m.
+Proof NZlt_ge_cases.
 
-Theorem le_nlt : forall n m : N, n <= m <-> ~ m < n.
-Proof NZle_nlt.
+Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m.
+Proof NZle_ngt.
 
-Theorem lt_dec : forall n m : N, n < m \/ ~ n < m.
-Proof NZlt_dec.
+Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m.
+Proof NZnlt_ge.
+
+Theorem lt_em : forall n m : N, n < m \/ ~ n < m.
+Proof NZlt_em.
 
 Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof NZlt_dne.
 
-Theorem nle_lt : forall n m : N, ~ n <= m <-> m < n.
-Proof NZnle_lt.
+Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m.
+Proof NZnle_gt.
+
+Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m.
+Proof NZlt_nge.
 
-Theorem le_dec : forall n m : N, n <= m \/ ~ n <= m.
-Proof NZle_dec.
+Theorem le_em : forall n m : N, n <= m \/ ~ n <= m.
+Proof NZle_em.
 
 Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m.
 Proof NZle_dne.
@@ -196,7 +202,7 @@ Proof NZle_ind.
 
 Theorem nlt_0_r : forall n : N, ~ n < 0.
 Proof.
-intro n; apply -> le_nlt. apply le_0_l.
+intro n; apply -> le_ngt. apply le_0_l.
 Qed.
 
 Theorem nle_succ_0 : forall n, ~ (S n <= 0).
@@ -382,9 +388,3 @@ Qed.
 
 End NOrderPropFunct.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NOtherInd.v b/theories/Numbers/Natural/Abstract/NOtherInd.v
index 9b01e5143..7faae620a 100644
--- a/theories/Numbers/Natural/Abstract/NOtherInd.v
+++ b/theories/Numbers/Natural/Abstract/NOtherInd.v
@@ -159,9 +159,3 @@ End Recursion.
 
 Implicit Arguments recursion [A].
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index f1e0e6ace..8ca3ba000 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -42,7 +42,7 @@ Proof NZplus_cancel_l.
 Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are valid for natural numbers but cannot be proved for N *)
+(** Theorems that are valid for natural numbers but cannot be proved for Z *)
 
 Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
@@ -135,9 +135,3 @@ Qed.
 
 End NPlusPropFunct.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index df4c94614..c4640858e 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -85,9 +85,3 @@ Qed.
 
 End NPlusOrderProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NPred.v b/theories/Numbers/Natural/Abstract/NPred.v
index 711d6b883..d3d22651c 100644
--- a/theories/Numbers/Natural/Abstract/NPred.v
+++ b/theories/Numbers/Natural/Abstract/NPred.v
@@ -44,9 +44,3 @@ Qed.
 
 End NDefPred.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index c35a6693b..d1f4aac26 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -67,9 +67,3 @@ Implicit Arguments strong_rec [A].
 
 End StrongRecProperties.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index a0d255892..bcf073ffa 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -39,7 +39,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-Lemma semi_ring : semi_ring_theory 0 1 NZplus NZtimes E.
+Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes E.
 Proof.
 constructor.
 exact plus_0_l.
@@ -52,7 +52,7 @@ exact times_assoc.
 exact times_plus_distr_r.
 Qed.
 
-Add Ring SR : semi_ring.
+Add Ring NSR : Nsemi_ring.
 
 (** Theorems that cannot be proved in NZTimes *)
 
@@ -112,9 +112,3 @@ Qed.
 
 End NTimesPropFunct.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 68c6c4494..2dbfd8f97 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -28,14 +28,23 @@ Proof NZplus_lt_le_mono.
 Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
 Proof NZplus_le_lt_mono.
 
-Theorem plus_le_lt_mono_opp : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
-Proof NZplus_le_lt_mono_opp.
+Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
+Proof NZle_lt_plus_lt.
 
-Theorem plus_lt_inv : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
-Proof NZplus_lt_inv.
+Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
+Proof NZlt_le_plus_lt.
 
-Theorem plus_gt_inv_0 : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZplus_gt_inv_0.
+Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_lt.
+
+Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
+Proof NZplus_lt_cases.
+
+Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Proof NZplus_le_cases.
+
+Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Proof NZplus_pos_cases.
 
 (** Theorems true for natural numbers *)
 
@@ -123,11 +132,12 @@ Proof NZtimes_eq_0.
 Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZtimes_neq_0.
 
-End NTimesOrderPropFunct.
+Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
+Proof.
+intros n m; split; [intro H | intros [H1 H2]].
+apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
+now apply times_pos_pos.
+Qed.
 
+End NTimesOrderPropFunct.
 
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 90b338773..557177907 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -194,9 +194,3 @@ end.
 *)
 (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 2f6c13cac..f8a9ecd63 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -172,9 +172,3 @@ End NPeanoAxiomsMod.
 
 Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
 
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 6d3ad55a9..7feed2b14 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -226,12 +226,15 @@ Ltac rewrite_true P H :=
 setoid_replace P with True using relation iff;
 [| split; intro; [constructor | apply H]].
 
-Tactic Notation "symmetry" constr(Eq) :=
+(*Ltac symmetry Eq :=
 lazymatch Eq with
 | ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff;
   [| split; intro; symmetry; assumption]
 | _ => fail Eq "does not have the form (E t1 t2)"
-end.
+end.*)
+(* This does not work because there already is a tactic "symmetry".
+Declaring "symmetry" a tactic notation does not work because it conflicts
+with "symmetry in": it thinks that "in" is a term. *)
 
 Theorem and_cancel_l : forall A B C : Prop,
   (B -> A) -> (C -> A ) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v
index a781411a2..e41052f95 100644
--- a/theories/Numbers/QRewrite.v
+++ b/theories/Numbers/QRewrite.v
@@ -104,8 +104,8 @@ lazymatch (type of H) with
     let x1 := fresh "x" in
     let x2 := fresh "x" in
     set (x1 := t1); set (x2 := t2);
-    assert (H1 : E x1 x2); [apply H |];
-    assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2); [qiff x1 x2 H1 |];
+    assert (H1 : E x1 x2) by apply H;
+    assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2) by qiff x1 x2 H1;
     unfold x1 in *; unfold x2 in *; apply <- H2;
     clear H1 H2 x1 x2
   | _ => pattern t1; qsetoid_rewrite H
@@ -114,11 +114,15 @@ lazymatch (type of H) with
 end.
 
 Tactic Notation "qsetoid_rewrite" "<-" constr(H) :=
-let H1 := fresh in
-  pose proof H as H1;
-  symmetry in H1;
-  qsetoid_rewrite H1;
-  clear H1.
+match goal with
+| |- ?G =>
+  let H1 := fresh in
+    pose proof H as H1;
+    symmetry in H1; (* symmetry unfolds the beta-redex in the goal (!), so we have to restore the goal *)
+    change G;
+    qsetoid_rewrite H1;
+    clear H1
+end.
 
 Tactic Notation "qsetoid_replace" constr(t1) "with" constr(t2)
                 "using" "relation" constr(E) :=
@@ -141,8 +145,19 @@ as E_rel.
 
 Notation "x == y" := (E x y) (at level 70).
 
+Parameter P : nat -> nat.
+Add Morphism S with signature E ==> E as S_morph. Admitted.
+Add Morphism P with signature E ==> E as P_morph. Admitted.
 Add Morphism plus with signature E ==> E ==> E as plus_morph. Admitted.
 
+Theorem Zplus_pred : forall n m : nat, P n + m == P (n + m).
+Proof.
+intros n m.
+cut (forall n : nat, S (P n) == n). intro H.
+pattern n at 2.
+qsetoid_rewrite <- (H n).
+Admitted.
+
 Goal forall x, x == x + x ->
   (exists y, forall z, y == y + z -> exists u, x == u) /\ x == 0.
 intros x H1. pattern x at 1.