Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

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

7 files changed, 349 insertions, 142 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index e81cffe4f3..fdc7bab4cb 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -45,9 +45,13 @@ Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
 
 Parameter Zopp : Z -> Z.
 
+(*Notation "- 1" := (Zopp 1) : IntScope.
+Check (-1).*)
+
 Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 
 Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope.
 
 Open Local Scope IntScope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index ace49428d2..db5bc99f92 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -10,10 +10,15 @@
 
 (*i i*)
 
+Require Export Decidable.
 Require Export ZAxioms.
 Require Import NZTimesOrder.
 
-Module ZBasePropFunct (Export ZAxiomsMod : ZAxiomsSig).
+Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
+
+(* Note: writing "Export" instead of "Import" on the previous line leads to
+some warnings about hiding repeated declarations and results in the loss of
+notations in Zplus and later *)
 
 Open Local Scope IntScope.
 
@@ -43,8 +48,8 @@ Proof NZsucc_inj_wd_neg.
 (* Decidability and stability of equality was proved only in NZOrder, but
 since it does not mention order, we'll put it here *)
 
-Theorem Zeq_em : forall n m : Z, n == m \/ n ~= m.
-Proof NZeq_em.
+Theorem Zeq_dec : forall n m : Z, decidable (n == m).
+Proof NZeq_dec.
 
 Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
 Proof NZeq_dne.
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 9b452039cb..a81b3a4196 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -34,14 +34,14 @@ Theorem Zmax_wd :
   forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
 Proof NZmax_wd.
 
-Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
-Proof NZle_lt_or_eq.
+Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof NZlt_eq_cases.
 
 Theorem Zlt_irrefl : forall n : Z, ~ n < n.
 Proof NZlt_irrefl.
 
-Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
-Proof NZlt_succ_le.
+Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m.
+Proof NZlt_succ_r.
 
 Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
 Proof NZmin_l.
@@ -63,44 +63,44 @@ Proof NZlt_le_incl.
 Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
 Proof NZlt_neq.
 
-Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
-Proof NZlt_le_neq.
+Theorem Zle_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
+Proof NZle_neq.
 
 Theorem Zle_refl : forall n : Z, n <= n.
 Proof NZle_refl.
 
-Theorem Zlt_succ_r : forall n : Z, n < S n.
-Proof NZlt_succ_r.
+Theorem Zlt_succ_diag_r : forall n : Z, n < S n.
+Proof NZlt_succ_diag_r.
 
-Theorem Zle_succ_r : forall n : Z, n <= S n.
-Proof NZle_succ_r.
+Theorem Zle_succ_diag_r : forall n : Z, n <= S n.
+Proof NZle_succ_diag_r.
 
-Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m.
-Proof NZlt_lt_succ.
+Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m.
+Proof NZlt_lt_succ_r.
 
-Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m.
-Proof NZle_le_succ.
+Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m.
+Proof NZle_le_succ_r.
 
-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 Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
+Proof NZle_succ_r.
 
-Theorem Zneq_succ_l : forall n : Z, S n ~= n.
-Proof NZneq_succ_l.
+Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n.
+Proof NZneq_succ_diag_l.
 
-Theorem Znlt_succ_l : forall n : Z, ~ S n < n.
-Proof NZnlt_succ_l.
+Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n.
+Proof NZneq_succ_diag_r.
 
-Theorem Znle_succ_l : forall n : Z, ~ S n <= n.
-Proof NZnle_succ_l.
+Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n.
+Proof NZnlt_succ_diag_l.
 
-Theorem Zlt_le_succ : forall n m : Z, n < m <-> S n <= m.
-Proof NZlt_le_succ.
+Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n.
+Proof NZnle_succ_diag_l.
 
-Theorem Zlt_succ_lt : forall n m : Z, S n < m -> n < m.
-Proof NZlt_succ_lt.
+Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m.
+Proof NZle_succ_l.
 
-Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m.
-Proof NZle_succ_le.
+Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m.
+Proof NZlt_succ_l.
 
 Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
 Proof NZsucc_lt_mono.
@@ -111,6 +111,8 @@ Proof NZsucc_le_mono.
 Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
 Proof NZlt_asymm.
 
+Notation Zlt_ngt := Zlt_asymm (only parsing).
+
 Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
 Proof NZlt_trans.
 
@@ -126,11 +128,16 @@ Proof NZlt_le_trans.
 Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
 Proof NZle_antisymm.
 
+Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m.
+Proof NZlt_1_l.
+
 (** Trichotomy, decidability, and double negation elimination *)
 
 Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
+Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing).
+
 Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
 Proof NZlt_gt_cases.
 
@@ -149,8 +156,8 @@ Proof NZle_ngt.
 Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
 Proof NZnlt_ge.
 
-Theorem Zlt_em : forall n m : Z, n < m \/ ~ n < m.
-Proof NZlt_em.
+Theorem Zlt_dec : forall n m : Z, decidable (n < m).
+Proof NZlt_dec.
 
 Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof NZlt_dne.
@@ -161,14 +168,14 @@ Proof NZnle_gt.
 Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
 Proof NZlt_nge.
 
-Theorem Zle_em : forall n m : Z, n <= m \/ ~ n <= m.
-Proof NZle_em.
+Theorem Zle_dec : forall n m : Z, decidable (n <= m).
+Proof NZle_dec.
 
 Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
 Proof NZle_dne.
 
-Theorem Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n.
-Proof NZlt_nlt_succ.
+Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m.
+Proof NZnlt_succ_r.
 
 Theorem Zlt_exists_pred :
   forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
@@ -307,17 +314,17 @@ Proof NZgt_wf.
 
 Theorem Zlt_pred_l : forall n : Z, P n < n.
 Proof.
-intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r.
+intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_diag_r.
 Qed.
 
 Theorem Zle_pred_l : forall n : Z, P n <= n.
 Proof.
-intro; le_less; apply Zlt_pred_l.
+intro; apply Zlt_le_incl; apply Zlt_pred_l.
 Qed.
 
 Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
 Proof.
-intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_le.
+intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_r.
 Qed.
 
 Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
@@ -328,17 +335,17 @@ Qed.
 Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
 Proof.
 intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
-apply Zlt_le_succ.
+symmetry; apply Zle_succ_l.
 Qed.
 
 Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
 Proof.
-intros; apply <- Zlt_pred_le; le_less.
+intros; apply <- Zlt_pred_le; now apply Zlt_le_incl.
 Qed.
 
 Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
 Proof.
-intros; le_less; now apply <- Zlt_pred_le.
+intros; apply Zlt_le_incl; now apply <- Zlt_pred_le.
 Qed.
 
 Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
@@ -348,7 +355,7 @@ Qed.
 
 Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
 Proof.
-intros; le_less; now apply <- Zlt_le_pred.
+intros; apply Zlt_le_incl; now apply <- Zlt_le_pred.
 Qed.
 
 Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
@@ -373,7 +380,7 @@ Qed.
 
 Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
 Proof.
-intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_le.
+intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_r.
 Qed.
 
 Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m.
@@ -386,5 +393,12 @@ Proof.
 intro; apply Zlt_neq; apply Zlt_pred_l.
 Qed.
 
+Theorem Zlt_n1_r : forall n m : Z, n < m -> m < 0 -> n < -1.
+Proof.
+intros n m H1 H2. apply -> Zlt_le_pred in H2.
+setoid_replace (P 0) with (-1) in H2. now apply NZlt_le_trans with m.
+apply <- Zeq_opp_r. now rewrite Zopp_pred, Zopp_0.
+Qed.
+
 End ZOrderPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index 16fe114313..b0cebd482d 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -85,7 +85,7 @@ intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m);
 apply Zplus_pred_l.
 Qed.
 
-Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m.
+Theorem Zplus_opp_r : forall n m : Z, n + (- m) == n - m.
 Proof.
 NZinduct m.
 rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r.
@@ -94,12 +94,12 @@ Qed.
 
 Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
 Proof.
-intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l.
+intro n; rewrite <- Zplus_opp_r; now rewrite Zplus_0_l.
 Qed.
 
 Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m).
 Proof.
-intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l.
+intros n m; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_succ_l.
 Qed.
 
 Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m).
@@ -127,24 +127,24 @@ now rewrite Zminus_0_r.
 intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem Zplus_opp_r : forall n : Z, n + (- n) == 0.
+Theorem Zplus_opp_diag_l : forall n : Z, - n + n == 0.
 Proof.
-intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag.
+intro n; now rewrite Zplus_comm, Zplus_opp_r, Zminus_diag.
 Qed.
 
-Theorem Zplus_opp_l : forall n : Z, - n + n == 0.
+Theorem Zplus_opp_diag_r : forall n : Z, n + (- n) == 0.
 Proof.
-intro n; rewrite Zplus_comm; apply Zplus_opp_r.
+intro n; rewrite Zplus_comm; apply Zplus_opp_diag_l.
 Qed.
 
-Theorem Zminus_swap : forall n m : Z, - m + n == n - m.
+Theorem Zplus_opp_l : forall n m : Z, - m + n == n - m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm.
+intros n m; rewrite <- Zplus_opp_r; now rewrite Zplus_comm.
 Qed.
 
 Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc.
+intros n m p; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_assoc.
 Qed.
 
 Theorem Zopp_involutive : forall n : Z, - (- n) == n.
@@ -164,7 +164,7 @@ Qed.
 
 Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr.
+intros n m; rewrite <- Zplus_opp_r, Zopp_plus_distr.
 now rewrite Zopp_involutive.
 Qed.
 
@@ -178,57 +178,163 @@ Proof.
 intros n m; split; [apply Zopp_inj | apply Zopp_wd].
 Qed.
 
+Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m.
+Proof.
+intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive.
+Qed.
+
+Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m.
+Proof.
+symmetry; apply Zeq_opp_l.
+Qed.
+
 Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
 Proof.
-intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc.
-now do 2 rewrite Zplus_opp_minus.
+intros n m p; rewrite <- Zplus_opp_r, Zopp_plus_distr, Zplus_assoc.
+now do 2 rewrite Zplus_opp_r.
 Qed.
 
 Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
 Proof.
-intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc.
-now rewrite Zplus_opp_minus.
+intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
+now rewrite Zplus_opp_r.
 Qed.
 
-Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m.
+Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive.
+intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive.
 Qed.
 
 Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc.
-now rewrite Zminus_swap.
+intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_r n p), <- Zplus_assoc.
+now rewrite Zplus_opp_l.
 Qed.
 
-Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n.
+Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
 Proof.
-intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc;
-rewrite Zminus_diag; now rewrite Zplus_0_r.
+intros n m p. rewrite <- (Zplus_cancel_l (n - m) (n - p) (- n)).
+do 2 rewrite Zplus_minus_assoc. rewrite Zplus_opp_diag_l; do 2 rewrite Zminus_0_l.
+apply Zopp_inj_wd.
 Qed.
 
-Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n.
+Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
 Proof.
-intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r.
+intros n m p.
+stepl (n - p + p == m - p + p) by apply Zplus_cancel_r.
+now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
 Qed.
 
-Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p.
+(* The next several theorems are devoted to moving terms from one side of
+an equation to the other. The name contains the operation in the original
+equation (plus or minus) and the indication whether the left or right term
+is moved. *)
+
+Theorem Zplus_move_l : forall n m p : Z, n + m == p <-> m == p - n.
 Proof.
 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.
+stepl (n + m - n == p - n) by apply Zminus_cancel_r.
+now rewrite Zplus_comm, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+Qed.
+
+Theorem Zplus_move_r : forall n m p : Z, n + m == p <-> n == p - m.
+Proof.
+intros n m p; rewrite Zplus_comm; now apply Zplus_move_l.
+Qed.
+
+(* The two theorems above do not allow rewriting subformulas of the form
+n - m == p to n == p + m since subtraction is in the right-hand side of
+the equation. Hence the following two theorems. *)
+
+Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
+Proof.
+intros n m p; rewrite <- (Zplus_opp_r n m); apply Zplus_move_l.
 Qed.
 
-Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m.
+Theorem Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m.
 Proof.
-intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l.
+intros n m p; rewrite <- (Zplus_opp_r n m). now rewrite Zplus_move_r, Zminus_opp_r.
 Qed.
 
-Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m.
+Theorem Zplus_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
 Proof.
-intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split.
+intros n m; now rewrite Zplus_move_l, Zminus_0_l.
 Qed.
 
+Theorem Zplus_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
+Proof.
+intros n m; now rewrite Zplus_move_r, Zminus_0_l.
+Qed.
+
+Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
+Proof.
+intros n m. now rewrite Zminus_move_l, Zminus_0_l.
+Qed.
+
+Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
+Proof.
+intros n m. now rewrite Zminus_move_r, Zplus_0_l.
+Qed.
+
+(* The following section is devoted to cancellation of like terms. The name
+includes the first operator and the position of the term being canceled. *)
+
+Theorem Zplus_simpl_l : forall n m : Z, n + m - n == m.
+Proof.
+intros; now rewrite Zplus_minus_swap, Zminus_diag, Zplus_0_l.
+Qed.
+
+Theorem Zplus_simpl_r : forall n m : Z, n + m - m == n.
+Proof.
+intros; now rewrite <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+Qed.
+
+Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m.
+Proof.
+intros; now rewrite <- Zplus_minus_swap, Zplus_opp_diag_l, Zminus_0_l.
+Qed.
+
+Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n.
+Proof.
+intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
+Qed.
+
+(* Now we have two sums or differences; the name includes the two operators
+and the position of the terms being canceled *)
+
+Theorem Zplus_plus_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
+Proof.
+intros n m p. now rewrite (Zplus_comm n m), <- Zplus_minus_assoc,
+Zminus_plus_distr, Zminus_diag, Zminus_0_l, Zplus_opp_r.
+Qed.
+
+Theorem Zplus_plus_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
+Proof.
+intros n m p. rewrite (Zplus_comm p n); apply Zplus_plus_simpl_l_l.
+Qed.
+
+Theorem Zplus_plus_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
+Proof.
+intros n m p. rewrite (Zplus_comm n m); apply Zplus_plus_simpl_l_l.
+Qed.
+
+Theorem Zplus_plus_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
+Proof.
+intros n m p. rewrite (Zplus_comm p m); apply Zplus_plus_simpl_r_l.
+Qed.
+
+Theorem Zminus_plus_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
+Proof.
+intros n m p. now rewrite <- Zminus_minus_distr, Zminus_plus_distr, Zminus_diag,
+Zminus_0_l, Zminus_opp_r.
+Qed.
+
+Theorem Zminus_plus_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
+Proof.
+intros n m p. rewrite (Zplus_comm p m); apply Zminus_plus_simpl_r_l.
+Qed.
+
+(* Of course, there are many other variants *)
+
 End ZPlusPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 01226b1218..ce79055a71 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -10,7 +10,7 @@
 
 (*i i*)
 
-Require Export ZOrder.
+Require Export ZLt.
 
 Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
@@ -94,25 +94,25 @@ Proof NZplus_nonneg_cases.
 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.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 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.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 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.
+do 2 rewrite Zplus_opp_r. 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.
+do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zle_le_minus.
 Qed.
 
 Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
@@ -137,13 +137,13 @@ 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.
+intros n m p. do 2 rewrite <- Zplus_opp_r. 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.
+intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_lt_mono_r.
 Qed.
 
 Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.
@@ -155,13 +155,13 @@ 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;
+intros n m p; do 2 rewrite <- Zplus_opp_r; 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.
+intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_le_mono_r.
 Qed.
 
 Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.
@@ -188,31 +188,31 @@ Qed.
 Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.
 Proof.
 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].
+[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r].
 Qed.
 
 Theorem Zlt_le_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.
 Proof.
 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].
+[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_r].
 Qed.
 
 Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
 intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n));
-[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
+[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r].
 Qed.
 
 Theorem Zlt_plus_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p.
 Proof.
 intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r.
-now rewrite Zplus_minus_diag.
+now rewrite Zplus_simpl_r.
 Qed.
 
 Theorem Zle_plus_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p.
 Proof.
 intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r.
-now rewrite Zplus_minus_diag.
+now rewrite Zplus_simpl_r.
 Qed.
 
 Theorem Zlt_plus_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n.
@@ -228,13 +228,13 @@ Qed.
 Theorem Zlt_minus_lt_plus_r : forall n m p : Z, n - p < m <-> n < m + p.
 Proof.
 intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zplus_lt_mono_r.
-now rewrite Zminus_plus_diag.
+now rewrite Zminus_simpl_r.
 Qed.
 
 Theorem Zle_minus_le_plus_r : forall n m p : Z, n - p <= m <-> n <= m + p.
 Proof.
 intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zplus_le_mono_r.
-now rewrite Zminus_plus_diag.
+now rewrite Zminus_simpl_r.
 Qed.
 
 Theorem Zlt_minus_lt_plus_l : forall n m p : Z, n - m < p <-> n < m + p.
@@ -281,32 +281,53 @@ Qed.
 
 Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
-intros n m H; rewrite <- Zplus_opp_minus in H.
+intros n m H; rewrite <- Zplus_opp_r 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 Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros n m H; rewrite <- Zplus_opp_minus in H.
+intros n m H; rewrite <- Zplus_opp_r 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 Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
-intros n m H; rewrite <- Zplus_opp_minus in H.
+intros n m H; rewrite <- Zplus_opp_r 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 Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
-intros n m H; rewrite <- Zplus_opp_minus in H.
+intros n m H; rewrite <- Zplus_opp_r in H.
 setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos).
 now apply Zplus_nonneg_cases.
 Qed.
 
+Section PosNeg.
+
+Variable P : Z -> Prop.
+Hypothesis P_wd : predicate_wd Zeq P.
+
+Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed.
+
+Theorem Z0_pos_neg :
+  P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.
+Proof.
+intros H1 H2 n. destruct (Zlt_trichotomy n 0) as [H3 | [H3 | H3]].
+apply <- Zopp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3].
+now rewrite Zopp_involutive in H3.
+now rewrite H3.
+apply H2 in H3; now destruct H3.
+Qed.
+
+End PosNeg.
+
+Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg).
+
 End ZPlusOrderPropFunct.
 
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 14c59fcfa0..89249d1ed9 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -10,7 +10,6 @@
 
 (*i i*)
 
-Require Export Ring.
 Require Export ZPlus.
 
 Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
@@ -21,20 +20,20 @@ Theorem Ztimes_wd :
   forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
 Proof NZtimes_wd.
 
-Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
-Proof NZtimes_0_r.
-
-Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
-Proof NZtimes_succ_r.
-
-(** Theorems that are valid for both natural numbers and integers *)
-
 Theorem Ztimes_0_l : forall n : Z, 0 * n == 0.
 Proof NZtimes_0_l.
 
 Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
 Proof NZtimes_succ_l.
 
+(** Theorems that are valid for both natural numbers and integers *)
+
+Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
+Proof NZtimes_0_r.
+
+Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Proof NZtimes_succ_r.
+
 Theorem Ztimes_comm : forall n m : Z, n * m == m * n.
 Proof NZtimes_comm.
 
@@ -44,6 +43,13 @@ Proof NZtimes_plus_distr_r.
 Theorem Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
 Proof NZtimes_plus_distr_l.
 
+(* A note on naming: right (correspondingly, left) distributivity happens
+when the sum is multiplied by a number on the right (left), not when the
+sum itself is the right (left) factor in the product (see planetmath.org
+and mathworld.wolfram.com). In the old library BinInt, distributivity over
+subtraction was named correctly, but distributivity over addition was named
+incorrectly. The names in Isabelle/HOL library are also incorrect. *)
+
 Theorem Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
 Proof NZtimes_assoc.
 
@@ -56,29 +62,11 @@ 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 Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_times_0.
 
-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 NZeq.
-Proof.
-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.
-
-Add Ring ZR : Zring.
+Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_times_0.
 
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
@@ -94,29 +82,32 @@ Proof.
 intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r.
 Qed.
 
-Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m).
+Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m).
 Proof.
-intros; ring.
+intros n m. apply -> Zplus_move_0_r.
+now rewrite <- Ztimes_plus_distr_r, Zplus_opp_diag_l, Ztimes_0_l.
 Qed.
 
-Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m).
+Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m).
 Proof.
-intros; ring.
+intros n m; rewrite (Ztimes_comm n (- m)), (Ztimes_comm n m); apply Ztimes_opp_l.
 Qed.
 
 Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
 Proof.
-intros; ring.
+intros n m; now rewrite Ztimes_opp_l, Ztimes_opp_r, Zopp_involutive.
 Qed.
 
-Theorem Ztimes_minus_distr_r : forall n m p : Z, n * (m - p) == n * m - n * p.
+Theorem Ztimes_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
 Proof.
-intros; ring.
+intros n m p. do 2 rewrite <- Zplus_opp_r. rewrite Ztimes_plus_distr_l.
+now rewrite Ztimes_opp_r.
 Qed.
 
-Theorem Ztimes_minus_distr_l : forall n m p : Z, (n - m) * p == n * p - m * p.
+Theorem Ztimes_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
 Proof.
-intros; ring.
+intros n m p; rewrite (Ztimes_comm (n - m) p), (Ztimes_comm n p), (Ztimes_comm m p);
+now apply Ztimes_minus_distr_l.
 Qed.
 
 End ZTimesPropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 1b9e9b5192..287fdb7f19 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -96,11 +96,20 @@ 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 Zlt_1_times_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m.
+Proof NZlt_1_times_pos.
 
-Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZtimes_neq_0.
+Theorem Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_times_0.
+
+Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_times_0.
+
+Theorem Zeq_times_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
+Proof NZeq_times_0_l.
+
+Theorem Zeq_times_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0.
+Proof NZeq_times_0_r.
 
 Theorem Ztimes_pos : forall n m : Z, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof NZtimes_pos.
@@ -114,7 +123,64 @@ Proof NZtimes_2_mono_l.
 
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
-(* None? *)
+Theorem Zlt_1_times_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
+Proof.
+intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
+apply <- Zopp_pos_neg in H2. rewrite Ztimes_opp_l, Ztimes_1_l in H1.
+now apply Zlt_1_l with (- m).
+assumption.
+Qed.
+
+Theorem Zlt_times_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1.
+Proof.
+intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
+rewrite Ztimes_1_l in H1. now apply Zlt_n1_r with m.
+assumption.
+Qed.
+
+Theorem Zlt_times_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1.
+Proof.
+intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1.
+rewrite Ztimes_opp_l, Ztimes_1_l in H1.
+apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
+assumption.
+Qed.
+
+Theorem Zlt_1_l_times : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Proof.
+intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
+left. now apply Zlt_times_n1_neg.
+right; left; now rewrite H1, Ztimes_0_r.
+right; right; now apply Zlt_1_times_pos.
+Qed.
+
+Theorem Zlt_n1_r_times : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Proof.
+intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
+right; right. now apply Zlt_1_times_neg.
+right; left; now rewrite H1, Ztimes_0_r.
+left. now apply Zlt_times_n1_pos.
+Qed.
+
+Theorem Zeq_times_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1.
+Proof.
+assert (F : ~ 1 < -1).
+intro H.
+assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r.
+assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l.
+Z0_pos_neg n.
+intros m H; rewrite Ztimes_0_l in H; false_hyp H Zneq_succ_diag_r.
+intros n H; split; apply <- Zle_succ_l in H; le_elim H.
+intros m H1; apply (Zlt_1_l_times n m) in H.
+rewrite H1 in H; destruct H as [H | [H | H]].
+false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl.
+intros; now left.
+intros m H1; apply (Zlt_1_l_times n m) in H. rewrite Ztimes_opp_l in H1;
+apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
+false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
+false_hyp H Zneq_succ_diag_l. false_hyp H F.
+intros; right; symmetry; now apply Zopp_wd.
+Qed.
 
 End ZTimesOrderPropFunct.