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

8 files changed, 132 insertions, 171 deletions

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.