BinInt: Z.add become the alternative Z.add'

 It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub.
 Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec.

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

12 files changed, 167 insertions, 231 deletions

diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
index 3cd9d4d3e..ca894027a 100644
--- a/plugins/setoid_ring/Cring_initial.v
+++ b/plugins/setoid_ring/Cring_initial.v
@@ -146,15 +146,11 @@ Ltac rsimpl := simpl;  set_cring_notations.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
+ gen_phiZ1 (Z.pos_sub x y)
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0.
   assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1.
   rewrite Pos.compare_antisym in H1.
@@ -181,10 +177,8 @@ Ltac rsimpl := simpl;  set_cring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  rewrite Pos.compare_antisym;simpl.
-  cring_rewrite match_compOpp.
-  cring_rewrite cring_add_comm.
-  apply gen_phiZ1_add_pos_neg.
+  rewrite gen_phiZ1_add_pos_neg.
+  cring_rewrite cring_add_comm. norm.
   cring_rewrite ARgen_phiPOS_add; norm.
  Qed.
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 766473c6f..6f4747dcf 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -732,6 +732,14 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
  Notation pow_pos_plus :=  (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
                         ARth.(ARmul_comm) ARth.(ARmul_assoc)).
 
+ Lemma Z_pos_sub_gt : forall p q, (p > q)%positive ->
+  Z.pos_sub p q = Zpos (p - q).
+ Proof.
+  intros. apply Z.pos_sub_gt. now apply Pos.gt_lt.
+ Qed.
+
+ Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
+
  Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
   match
       (if  PExpr_eq e1 e2 then
@@ -751,6 +759,7 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
 Proof.
   intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
    case (PExpr_eq e1 e2); simpl; auto; intros H.
+  rewrite Z.pos_sub_spec.
   case_eq ((p1 ?= p2)%positive);intros;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).
@@ -763,22 +772,17 @@ Proof.
   rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
   rewrite H;trivial.
-   change (ZtoN
-     match (p1 ?= p1 - p2)%positive with
-     | Eq => 0
-     | Lt => Zneg (p1 - p2 - p1)
-     | Gt => Zpos (p1 - (p1 - p2))
-     end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
+   change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z.
   replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
   split.
   repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
-  rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
+  rewrite Zplus_assoc, Z.add_opp_diag_r. simpl.
   ring [ (morph1 CRmorph)].
  assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
  apply Zplus_gt_reg_l with (Zpos p2).
  rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
  apply Zplus_gt_compat_r. refine (refl_equal _).
- simpl;rewrite H0;trivial.
+ simpl. now simpl_pos_sub.
 Qed.
 
 Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
@@ -808,7 +812,7 @@ destruct n.
   destruct n;simpl.
     rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
     intros (H1,H2) (H3,H4).
-    unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
+    simpl_pos_sub. simpl in H3.
     rewrite pow_pos_mul. rewrite H1;rewrite H3.
     assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
         (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
@@ -818,11 +822,10 @@ destruct n.
    split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
    repeat rewrite pow_th.(rpow_pow_N);simpl.
    intros (H1,H2) (H3,H4).
-   unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
-   rewrite H2 in H1;simpl in H1.
+   simpl_pos_sub. simpl in H1, H3.
    assert (Zpos p1 > Zpos p6)%Z.
      apply Zgt_trans with (Zpos p4). exact H4. exact H2.
-  unfold Zgt in H;simpl in H;rewrite H.
+  simpl_pos_sub.
   split. 2:exact H.
   rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
   assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
@@ -835,12 +838,12 @@ destruct n.
   assert
      (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
  change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)%Z).
- simpl. rewrite Pcompare_refl. simpl. reflexivity.
+ rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
+ simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
  unfold Zminus, Zopp in H0. simpl in H0.
-  rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
+  simpl_pos_sub. inversion H0; trivial.
  simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
+ intros H1 (H2,H3). simpl_pos_sub.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
  rewrite pow_pos_mul. split. ring [H2]. exact H3.
@@ -851,8 +854,7 @@ destruct n.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
  intros (H1, H2);rewrite H1;split.
-   unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
-   simpl in H1;ring [H1]. trivial.
+   simpl_pos_sub. simpl in H1;ring [H1]. trivial.
  trivial.
  destruct n. trivial.
  generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
@@ -910,8 +912,7 @@ Proof.
      repeat rewrite NPEpow_correct;simpl;
      repeat rewrite pow_th.(rpow_pow_N);simpl).
   intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
-  intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
-  simpl in H;split;try ring [H].
+  intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
   rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
   simpl;intros. repeat rewrite NPEmul_correct;simpl.
   rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 56935bb79..9e4ac94b4 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -170,16 +170,11 @@ Section ZMORPHISM.
   rewrite H1;rrefl.
  Qed.
 
- Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
- == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Lemma gen_phiZ1_pos_sub : forall x y,
+ gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   case Pos.compare_spec; intros H; simpl.
   rewrite H. rewrite (Ropp_def Rth);rrefl.
   rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
@@ -190,21 +185,13 @@ Section ZMORPHISM.
   add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
  Qed.
 
- Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
-  match CompOpp x with Eq => be | Lt => bl | Gt => bg end
-  = match x with Eq => be | Lt => bg | Gt => bl end.
- Proof. destruct x;simpl;intros;trivial. Qed.
-
  Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
  Proof.
   intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
-  induction x;destruct y;simpl;norm.
+  destruct x, y; simpl; norm.
   apply (ARgen_phiPOS_add ARth).
-  apply gen_phiZ1_add_pos_neg.
-  rewrite Pos.compare_antisym.
-  rewrite match_compOpp.
-  rewrite (Radd_comm Rth).
-  apply gen_phiZ1_add_pos_neg.
+  apply gen_phiZ1_pos_sub.
+  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
   rewrite (ARgen_phiPOS_add ARth); norm.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v
index f94ad9b0f..7c5631d4e 100644
--- a/plugins/setoid_ring/Ring2_initial.v
+++ b/plugins/setoid_ring/Ring2_initial.v
@@ -146,15 +146,11 @@ Ltac rsimpl := simpl;  set_ring_notations.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
+ gen_phiZ1 (Z.pos_sub x y)
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0.
   assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1.
   rewrite Pos.compare_antisym in H1.
@@ -181,11 +177,8 @@ Ltac rsimpl := simpl;  set_ring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite Pos.compare_antisym;simpl.
-  ring_rewrite match_compOpp.
-  ring_rewrite ring_add_comm.
-  apply gen_phiZ1_add_pos_neg.
+  rewrite gen_phiZ1_add_pos_neg.
+  ring_rewrite ring_add_comm. norm.
   ring_rewrite ARgen_phiPOS_add; norm.
  Qed.
 
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 188a74fdd..b05ee6495 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -136,9 +136,9 @@ Proof.
 intros a [|n|n] [|m|m] H; simpl; try ring;
 try rewrite Qpower_plus_positive;
 try apply Qinv_mult_distr; try reflexivity;
-case_eq ((n ?= m)%positive); intros H0; simpl;
+rewrite ?Z.pos_sub_spec;
+case Pos.compare_spec; intros H0; simpl; subst;
  try rewrite Qpower_minus_positive;
- try rewrite (Pcompare_Eq_eq _ _ H0);
  try (field; try split; apply Qpower_not_0_positive);
  try assumption;
  apply ZC2;
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index de41fd3f6..70f4ff0d9 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1717,7 +1717,8 @@ Qed.
 Lemma plus_IZR_NEG_POS :
   forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
 Proof.
-  intros p q; simpl. case Pcompare_spec; intros H; simpl.
+  intros p q; simpl. rewrite Z.pos_sub_spec.
+  case Pcompare_spec; intros H; simpl.
   subst. ring.
   rewrite Pminus_minus by trivial.
   rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 1eee8d852..c0cd78649 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -557,6 +557,7 @@ Proof.
 (* POS/POS *)
   rewrite Pplus_plus; auto with real.
 (* POS/NEG *)
+  rewrite Z.pos_sub_spec.
   case Pcompare_spec; intros; simpl.
   subst; auto with real.
   rewrite Pminus_minus by trivial.
@@ -568,16 +569,17 @@ Proof.
   rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
   reflexivity.
 (* NEG/POS *)
+  rewrite Z.pos_sub_spec.
   case Pcompare_spec; intros; simpl.
   subst; auto with real.
   rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  auto with real.
-  rewrite Pminus_minus by trivial.
   rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
   rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
   rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+  rewrite Pminus_minus by trivial.
+  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
+  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+  auto with real.
 (* NEG/NEG *)
   rewrite Pplus_plus; auto with real.
   intros H'; rewrite pow_add; auto with real.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index b9ae45110..62f5a0f78 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -69,11 +69,18 @@ Proof.
  decide equality; apply Pos.eq_dec.
 Defined.
 
-(** * Equivalence with alternative [add'] [succ'] [pred'] *)
+(** * Properties of [pos_sub] *)
 
-(** ** Caracterisation of [pos_sub] *)
+(** [pos_sub] can be written in term of positive comparison
+    and subtraction (cf. earlier definition of addition of Z) *)
 
-Lemma pos_sub_spec p q : pos_sub p q = Zpos p + Zneg q.
+Lemma pos_sub_spec p q :
+ pos_sub p q =
+ match (p ?= q)%positive with
+   | Eq => 0
+   | Lt => Zneg (q - p)
+   | Gt => Zpos (p - q)
+ end.
 Proof.
  revert q. induction p; destruct q; simpl; trivial;
  rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI,
@@ -84,24 +91,29 @@ Proof.
   subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag.
 Qed.
 
-Lemma add_add' n m : n + m = add' n m.
+(** Particular cases of the previous result *)
+
+Lemma pos_sub_diag p : pos_sub p p = 0.
 Proof.
- symmetry.
- destruct n as [|n|n], m as [|m|m]; simpl add'; rewrite ?pos_sub_spec;
-  trivial.
- simpl. rewrite Pos.compare_antisym. now case Pos.compare.
+ now rewrite pos_sub_spec, Pos.compare_refl.
 Qed.
 
-Lemma succ_succ' n : succ n = succ' n.
+Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = Zneg (q - p).
 Proof.
- unfold succ. rewrite add_add'. destruct n; trivial.
- simpl. f_equal. apply Pos.add_1_r.
+ intros H. now rewrite pos_sub_spec, H.
 Qed.
 
-Lemma pred_pred' n : pred n = pred' n.
+Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q).
 Proof.
- unfold pred. rewrite add_add'. destruct n; trivial.
- simpl. f_equal. apply Pos.add_1_r.
+ intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H.
+Qed.
+
+(** The opposite of [pos_sub] is [pos_sub] with reversed arguments *)
+
+Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.
+Proof.
+ revert q; induction p; destruct q; simpl; trivial;
+ rewrite <- IHp; now destruct pos_sub.
 Qed.
 
 (** * Results concerning [Zpos] and [Zneg] and the operators *)
@@ -131,9 +143,19 @@ Proof.
  reflexivity.
 Qed.
 
+Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p.
+Proof.
+ reflexivity.
+Qed.
+
 Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n).
 Proof.
- intros H. simpl. now rewrite Pos.compare_antisym, H.
+ intros H. simpl. now apply pos_sub_gt.
 Qed.
 
 Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q).
@@ -196,7 +218,6 @@ Qed.
 
 Lemma add_comm n m : n + m = m + n.
 Proof.
- rewrite !add_add'.
  destruct n, m; simpl; trivial; now rewrite Pos.add_comm.
 Qed.
 
@@ -204,57 +225,57 @@ Qed.
 
 Lemma opp_add_distr n m : - (n + m) = - n + - m.
 Proof.
-  destruct n, m; simpl; trivial; now case Pos.compare_spec.
+ destruct n, m; simpl; trivial using pos_sub_opp.
+Qed.
+
+(** ** Opposite is injective *)
+
+Lemma opp_inj n m : -n = -m -> n = m.
+Proof.
+ destruct n, m; simpl; intros H; destr_eq H; now f_equal.
 Qed.
 
 (** ** Addition is associative *)
 
-Lemma add_assoc_pos (p q:positive)(n:Z) :
-  Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
+Lemma pos_sub_add p q r :
+  pos_sub (p + q) r = Zpos p + pos_sub q r.
 Proof.
- destruct n as [|n|n]; simpl; trivial.
- now rewrite Pos.add_assoc.
- case Pos.compare_spec; intros E0.
- (* y = z *)
+ simpl. rewrite !pos_sub_spec.
+ case (Pos.compare_spec q r); intros E0.
+ (* q = r *)
  subst.
- assert (H := Pos.lt_add_r n p).
+ assert (H := Pos.lt_add_r r p).
  rewrite Pos.add_comm in H. apply Pos.lt_gt in H.
  now rewrite H, Pos.add_sub.
- (* y < z *)
- assert (Hz : (n = (n-q)+q)%positive) by (now rewrite Pos.sub_add).
- rewrite Hz at 4. rewrite Pos.add_compare_mono_r.
+ (* q < r *)
+ rewrite pos_sub_spec.
+ assert (Hr : (r = (r-q)+q)%positive) by (now rewrite Pos.sub_add).
+ rewrite Hr at 1. rewrite Pos.add_compare_mono_r.
  case Pos.compare_spec; intros E1; trivial; f_equal.
- symmetry. rewrite Pos.add_comm. apply Pos.sub_add_distr.
- rewrite Hz, Pos.add_comm. now apply Pos.add_lt_mono_r.
- apply Pos.sub_sub_distr; trivial.
- (* z < y *)
- assert (LT : (n < p + q)%positive).
+ rewrite Pos.add_comm. apply Pos.sub_add_distr.
+ rewrite Hr, Pos.add_comm. now apply Pos.add_lt_mono_r.
+ symmetry. apply Pos.sub_sub_distr; trivial.
+ (* r < q *)
+ assert (LT : (r < p + q)%positive).
   apply Pos.lt_trans with q; trivial. rewrite Pos.add_comm. apply Pos.lt_add_r.
  apply Pos.lt_gt in LT. rewrite LT. f_equal.
- now apply Pos.add_sub_assoc.
+ symmetry. now apply Pos.add_sub_assoc.
 Qed.
 
 Lemma add_assoc n m p : n + (m + p) = n + m + p.
 Proof.
- destruct n as [|x|x], m as [|y|y], p as [|z|z]; trivial.
- apply add_assoc_pos.
- apply add_assoc_pos.
- now rewrite !add_0_r.
- rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
-  f_equal; apply add_comm.
- rewrite <- !opp_Zpos, <- (opp_Zneg x), <- !opp_add_distr. f_equal.
-  rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
-  now rewrite add_assoc_pos.
- now rewrite !add_0_r.
- rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
-  now rewrite add_assoc_pos.
- rewrite <- !opp_Zpos, <- (opp_Zneg y), <- !opp_add_distr. f_equal.
- rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
-  f_equal; apply add_comm.
- rewrite <- !opp_Zpos, <- (opp_Zneg z), <- !opp_add_distr. f_equal.
-  apply add_assoc_pos.
- rewrite <- !opp_Zpos, <- !opp_add_distr. f_equal.
-  apply add_assoc_pos.
+ assert (AUX : forall x y z, Zpos x + (y + z) = Zpos x + y + z).
+  intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial.
+  simpl. now rewrite Pos.add_assoc.
+  simpl (_ + Zneg _). symmetry. apply pos_sub_add.
+  simpl (Zneg _ + _); simpl (_ + Zneg _).
+  now rewrite (add_comm _ (Zpos _)), <- 2 pos_sub_add, Pos.add_comm.
+  apply opp_inj. rewrite !opp_add_distr, opp_Zpos, !opp_Zneg.
+  simpl (Zneg _ + _); simpl (_ + Zneg _).
+  rewrite add_comm, Pos.add_comm. apply pos_sub_add.
+ (* main *)
+ destruct n as [|n|n]. trivial. apply AUX.
+ apply opp_inj. rewrite !opp_add_distr, opp_Zneg. apply AUX.
 Qed.
 
 (** ** Subtraction and successor *)
@@ -268,7 +289,7 @@ Qed.
 
 Lemma add_opp_diag_r n : n + - n = 0.
 Proof.
- destruct n; simpl; trivial; now rewrite Pos.compare_refl.
+ destruct n; simpl; trivial; now rewrite pos_sub_diag.
 Qed.
 
 Lemma add_opp_diag_l n : - n + n = 0.
@@ -330,8 +351,8 @@ Lemma mul_add_distr_pos (p:positive) n m :
  Zpos p * (n + m) = Zpos p * n + Zpos p * m.
 Proof.
  destruct n as [|n|n], m as [|m|m]; simpl; trivial;
- rewrite ?Pos.mul_compare_mono_l; try case Pos.compare_spec; intros;
- now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
+ rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec;
+ intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
 Qed.
 
 Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
@@ -384,7 +405,7 @@ Qed.
 
 Lemma opp_succ n : -(succ n) = pred (-n).
 Proof.
- unfold succ, pred. destruct n; simpl; trivial. now case Pos.compare_spec.
+ unfold succ, pred. apply opp_add_distr.
 Qed.
 
 (** ** Specification of successor and predecessor *)
@@ -451,8 +472,8 @@ Qed.
 
 Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).
 Proof.
- destruct n as [|n|n], m as [|m|m]; simpl; trivial.
- case Pos.compare_spec; trivial.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial;
+ rewrite <- ? Pos.compare_antisym, ?pos_sub_spec;
  case Pos.compare_spec; trivial.
 Qed.
 
@@ -675,7 +696,7 @@ Lemma odd_spec n : odd n = true <-> Odd n.
 Proof.
  split.
  exists (div2 n). destruct n as [|[ | | ]|[ | | ]]; simpl; try easy.
- now rewrite Pos.double_succ, Pos.sub_1_r, Pos.pred_succ.
+ now rewrite Pos.pred_double_succ.
  intros (m,->). now destruct m as [|[ | | ]|[ | | ]].
 Qed.
 
@@ -797,7 +818,7 @@ Proof.
  now split.
  split. unfold le.
   now rewrite <- compare_antisym, <- compare_sub, compare_antisym, Hr'.
- unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
+ unfold lt in *; simpl in *. rewrite pos_sub_gt by trivial.
  simpl. now apply Pos.sub_decr.
 Qed.
 
@@ -813,8 +834,8 @@ Proof.
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
  split.
- unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
- simpl. rewrite <- Pos.compare_antisym. now apply Pos.sub_decr.
+ unfold lt in *; simpl in *. rewrite pos_sub_lt by trivial.
+ rewrite <- Pos.compare_antisym. now apply Pos.sub_decr.
  change (Zneg b - Zneg r <= 0). unfold le, lt in *.
   rewrite <- compare_sub. simpl in *.
   now rewrite <- Pos.compare_antisym, Hr'.
@@ -1093,7 +1114,7 @@ Proof.
   red. now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
  assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos n)%N).
   red in H. simpl in H. simpl to_N.
-  rewrite Pos.compare_antisym.
+  rewrite pos_sub_spec, Pos.compare_antisym.
   destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H).
   subst. now rewrite N.sub_diag.
   simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-).
@@ -1207,49 +1228,23 @@ Proof.
  destruct n. trivial. simpl. now rewrite Pos.add_1_r.
 Qed.
 
-(** ** Properties of [succ'] and [pred'] *)
-
-Lemma succ'_pred' n : succ' (pred' n) = n.
-Proof.
- rewrite <- succ_succ', <- pred_pred'. apply succ_pred.
-Qed.
-
-Lemma pred'_succ' n : pred' (succ' n) = n.
-Proof.
- rewrite <- succ_succ', <- pred_pred'. apply pred_succ.
-Qed.
-
-Lemma succ'_inj n m : succ' n = succ' m -> n = m.
-Proof.
- intros H. now rewrite <- (pred'_succ' n), <- (pred'_succ' m), H.
-Qed.
-
-Lemma pred'_inj n m : pred' n = pred' m -> n = m.
-Proof.
- intros H. now rewrite <- (succ'_pred' n), <- (succ'_pred' m), H.
-Qed.
-
-Lemma neq_succ'_diag_r n : n <> succ' n.
-Proof.
- rewrite <- succ_succ'. rewrite <- compare_eq_iff.
- rewrite compare_sub, sub_succ_r. unfold sub. now rewrite add_opp_diag_r.
-Qed.
-
 (** ** Induction principles based on successor / predecessor *)
 
 Lemma peano_ind (P : Z -> Prop) :
   P 0 ->
-  (forall x, P x -> P (succ' x)) ->
-  (forall x, P x -> P (pred' x)) ->
+  (forall x, P x -> P (succ x)) ->
+  (forall x, P x -> P (pred x)) ->
   forall z, P z.
 Proof.
  intros H0 Hs Hp z; destruct z.
  assumption.
  induction p using Pos.peano_ind.
   now apply (Hs 0).
+  rewrite <- Pos.add_1_r.
   now apply (Hs (Zpos p)).
  induction p using Pos.peano_ind.
   now apply (Hp 0).
+  rewrite <- Pos.add_1_r.
   now apply (Hp (Zneg p)).
 Qed.
 
@@ -1261,8 +1256,8 @@ Lemma bi_induction (P : Z -> Prop) :
 Proof.
  intros _ H0 Hs. induction z using peano_ind.
  assumption.
- rewrite <- succ_succ'. now apply -> Hs.
- rewrite <- pred_pred'. apply Hs. now rewrite succ_pred.
+ now apply -> Hs.
+ apply Hs. now rewrite succ_pred.
 Qed.
 
 
@@ -1403,7 +1398,10 @@ Notation Zdouble_plus_one := Z.succ_double (only parsing).
 Notation Zdouble_minus_one := Z.pred_double (only parsing).
 Notation Zdouble := Z.double (only parsing).
 Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zplus := Z.add (only parsing).
+Notation Zsucc' := Z.succ (only parsing).
+Notation Zpred' := Z.pred (only parsing).
+Notation Zplus' := Z.add (only parsing).
+Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
 Notation Zopp := Z.opp (only parsing).
 Notation Zsucc := Z.succ (only parsing).
 Notation Zpred := Z.pred (only parsing).
@@ -1411,9 +1409,6 @@ Notation Zminus := Z.sub (only parsing).
 Notation Zmult := Z.mul (only parsing).
 Notation Zcompare := Z.compare (only parsing).
 Notation Zsgn := Z.sgn (only parsing).
-Notation Zsucc' := Z.succ' (only parsing).
-Notation Zpred' := Z.pred' (only parsing).
-Notation Zplus' := Z.add' (only parsing).
 Notation Zle := Z.le (only parsing).
 Notation Zge := Z.ge (only parsing).
 Notation Zlt := Z.lt (only parsing).
@@ -1445,13 +1440,11 @@ Notation Zplus_succ_l := Z.add_succ_l (only parsing).
 Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
 Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
 Notation Zsucc_inj := Z.succ_inj (only parsing).
-Notation Zsucc_succ' := Z.succ_succ' (only parsing).
-Notation Zpred_pred' := Z.pred_pred' (only parsing).
-Notation Zsucc'_inj := Z.succ'_inj (only parsing).
-Notation Zsucc'_pred' := Z.succ'_pred' (only parsing).
-Notation Zpred'_succ' := Z.pred'_succ' (only parsing).
-Notation Zpred'_inj := Z.pred'_inj (only parsing).
-Notation Zsucc'_discr := Z.neq_succ'_diag_r (only parsing).
+Notation Zsucc'_inj := Z.succ_inj (only parsing).
+Notation Zsucc'_pred' := Z.succ_pred (only parsing).
+Notation Zpred'_succ' := Z.pred_succ (only parsing).
+Notation Zpred'_inj := Z.pred_inj (only parsing).
+Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
 Notation Zminus_0_r := Z.sub_0_r (only parsing).
 Notation Zminus_diag := Z.sub_diag (only parsing).
 Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
@@ -1576,6 +1569,8 @@ Zplus_0_simpl_l
 Zplus_0_simpl_l_reverse
 Zplus_opp_expand
 Zsucc_inj_contrapositive
+Zsucc_succ'
+Zpred_pred'
 *)
 
 (* No compat notation for :
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index b0fef2a9d..4c2a19f69 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -51,26 +51,30 @@ Definition pred_double x :=
     | Zpos p => Zpos (Pos.pred_double p)
   end.
 
+(** ** Subtraction of positive into Z *)
+
+Fixpoint pos_sub (x y:positive) {struct y} : Z :=
+  match x, y with
+    | p~1, q~1 => double (pos_sub p q)
+    | p~1, q~0 => succ_double (pos_sub p q)
+    | p~1, 1 => Zpos p~0
+    | p~0, q~1 => pred_double (pos_sub p q)
+    | p~0, q~0 => double (pos_sub p q)
+    | p~0, 1 => Zpos (Pos.pred_double p)
+    | 1, q~1 => Zneg q~0
+    | 1, q~0 => Zneg (Pos.pred_double q)
+    | 1, 1 => Z0
+  end%positive.
+
 (** ** Addition *)
 
 Definition add x y :=
   match x, y with
     | 0, y => y
-    | Zpos x', 0 => Zpos x'
-    | Zneg x', 0 => Zneg x'
+    | x, 0 => x
     | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' =>
-      match (x' ?= y')%positive with
-	| Eq => 0
-	| Lt => Zneg (y' - x')
-	| Gt => Zpos (x' - y')
-      end
-    | Zneg x', Zpos y' =>
-      match (x' ?= y')%positive with
-	| Eq => 0
-	| Lt => Zpos (y' - x')
-	| Gt => Zneg (x' - y')
-      end
+    | Zpos x', Zneg y' => pos_sub x' y'
+    | Zneg x', Zpos y' => pos_sub y' x'
     | Zneg x', Zneg y' => Zneg (x' + y')
   end.
 
@@ -115,47 +119,6 @@ Definition mul x y :=
 
 Infix "*" := mul : Z_scope.
 
-(** ** Subtraction of positive into Z *)
-
-Fixpoint pos_sub (x y:positive) {struct y} : Z :=
-  match x, y with
-    | p~1, q~1 => double (pos_sub p q)
-    | p~1, q~0 => succ_double (pos_sub p q)
-    | p~1, 1 => Zpos p~0
-    | p~0, q~1 => pred_double (pos_sub p q)
-    | p~0, q~0 => double (pos_sub p q)
-    | p~0, 1 => Zpos (Pos.pred_double p)
-    | 1, q~1 => Zneg q~0
-    | 1, q~0 => Zneg (Pos.pred_double q)
-    | 1, 1 => Z0
-  end%positive.
-
-(** ** Direct, easier to handle variants of successor and addition *)
-
-Definition succ' x :=
-  match x with
-    | 0 => 1
-    | Zpos x' => Zpos (Pos.succ x')
-    | Zneg x' => pos_sub 1 x'
-  end.
-
-Definition pred' x :=
-  match x with
-    | 0 => -1
-    | Zpos x' => pos_sub x' 1
-    | Zneg x' => Zneg (Pos.succ x')
-  end.
-
-Definition add' x y :=
-  match x, y with
-    | 0, y => y
-    | x, 0 => x
-    | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' => pos_sub x' y'
-    | Zneg x', Zpos y' => pos_sub y' x'
-    | Zneg x', Zneg y' => Zneg (x' + y')
-  end.
-
 (** ** Power function *)
 
 Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index ef91f2d77..d37a6a9c3 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -169,7 +169,7 @@ Lemma Zdiv2_odd_eqn : forall n,
  n = 2*(Zdiv2 n) + if Zodd_bool n then 1 else 0.
 Proof.
  intros [ |[p|p| ]|[p|p|  ]]; simpl; trivial.
- f_equal. now rewrite xO_succ_permute, <-Ppred_minus, Ppred_succ.
+ f_equal. symmetry. apply Pos.pred_double_succ.
 Qed.
 
 Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index a4b5390e3..87a14a136 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -97,7 +97,7 @@ Qed.
 
 Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
 Proof.
-  intros; simpl. case Pos.compare_spec; intros H.
+  intros; simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros H.
   now rewrite H, Pos.sub_diag.
   rewrite Pminus_Lt; auto.
   symmetry. apply Zpos_max_1.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 454f62aa9..353ab602e 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -318,7 +318,7 @@ Qed.
 
 Lemma Z_of_N_minus : forall n m, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
 Proof.
- intros [|n] [|m]; simpl; trivial.
+ intros [|n] [|m]; simpl; trivial. rewrite Z.pos_sub_spec.
  case Pcompare_spec; intros H.
  subst. now rewrite Pminus_mask_diag.
  rewrite Pminus_mask_Lt; trivial.