Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits

Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.

Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)

PArith/BinPos:
 - added a power function Ppow
 - iterator iter_pos moved from Zmisc to here + some lemmas
 - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
 - more lemmas on Pcompare and succ/+/* and order, allow
   to simplify a lot some old proofs elsewhere.
 - new/revised results on Pminus (including some direct proof of
   stuff from Pnat)

PArith/Pnat:
 - more direct proofs (limit the need of stuff about Pmult_nat).
 - provide nicer names for some lemmas (eg. Pplus_plus instead of
   nat_of_P_plus_morphism), compatibility notations provided.
 - kill some too-specific lemmas unused in stdlib + contribs

NArith/BinNat:
 - N_of_nat, nat_of_N moved from Nnat to here.
 - a lemma relating Npred and Nminus
 - revised definitions and specification proofs of Npow and Nlog2

NArith/Nnat:
 - shorter proofs.
 - stuff about Z_of_N is moved to Znat. This way, NArith is
   entirely independent from ZArith.

NArith/Ndigits:
 - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
 - revised proofs about Nxor, still using functional bit stream
 - use the same approach to prove properties of Nand Nor Ndiff

ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff

ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat

ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N

ZArith/Zmisc: almost empty new, only contain stuff about badly-named
 iter. Should be reformed more someday.

ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
 proofs and avoid slowdown due to adding 1 in Z instead of in positive

Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
 as long as I dont't know why it's slower on powers of two.

Elsewhere: propagate new names + some nicer proofs

NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.

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

11 files changed, 468 insertions, 758 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index c39edf30f..b99a28d5f 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -11,11 +11,8 @@
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
-Require Export BinPos.
-Require Export Pnat.
-Require Import BinNat.
-Require Import Plus.
-Require Import Mult.
+Require Export BinPos Pnat.
+Require Import BinNat Plus Mult.
 
 Unset Boxed Definitions.
 
@@ -209,10 +206,10 @@ Proof.
   intros P H0 Hs Hp z; destruct z.
   assumption.
   apply Pind with (P := fun p => P (Zpos p)).
-    change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0.
+    change (P (Zsucc' Z0)); apply Hs; apply H0.
     intro n; exact (Hs (Zpos n)).
   apply Pind with (P := fun p => P (Zneg p)).
-    change (P (Zpred' Z0)) in |- *; apply Hp; apply H0.
+    change (P (Zpred' Z0)); apply Hp; apply H0.
     intro n; exact (Hp (Zneg n)).
 Qed.
 
@@ -245,7 +242,7 @@ Qed.
 
 Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.
 Proof.
-  intros x y; case x; case y; simpl in |- *; intros;
+  intros x y; case x; case y; simpl; intros;
     [ trivial
       | discriminate H
       | discriminate H
@@ -286,11 +283,10 @@ Qed.
 
 Theorem Zplus_comm : forall n m:Z, n + m = m + n.
 Proof.
-  intro x; induction x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl in |- *; try reflexivity.
+  induction n as [|p|p]; intros [|q|q]; simpl; try reflexivity.
   rewrite Pplus_comm; reflexivity.
-  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
-  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
+  rewrite ZC4. now case Pcompare_spec.
+  rewrite ZC4; now case Pcompare_spec.
   rewrite Pplus_comm; reflexivity.
 Qed.
 
@@ -299,7 +295,7 @@ Qed.
 Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 Proof.
   intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq);
+    simpl; reflexivity || destruct ((p ?= q)%positive Eq);
       reflexivity.
 Qed.
 
@@ -312,7 +308,7 @@ Qed.
 
 Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
 Proof.
-  intro x; destruct x as [| p| p]; simpl in |- *;
+  intro x; destruct x as [| p| p]; simpl;
     [ reflexivity
       | rewrite (Pcompare_refl p); reflexivity
       | rewrite (Pcompare_refl p); reflexivity ].
@@ -330,159 +326,54 @@ Hint Local Resolve Zplus_0_l Zplus_0_r.
 Lemma weak_assoc :
   forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
 Proof.
-  intros x y z'; case z';
-    [ auto with arith
-      | intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith
-      | intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0;
-	ElimPcompare (x + y)%positive z; intros E1; rewrite E1;
-	  [ absurd ((x + y ?= z)%positive Eq = Eq);
-	    [  (* Case 1 *)
-              rewrite nat_of_P_gt_Gt_compare_complement_morphism;
-		[ discriminate
-		  | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
-		    elim (ZL4 x); intros k E2; rewrite E2;
-		      simpl in |- *; unfold gt, lt in |- *;
-			apply le_n_S; apply le_plus_r ]
-	      | assumption ]
-	    | absurd ((x + y ?= z)%positive Eq = Lt);
-	      [  (* Case 2 *)
-		rewrite nat_of_P_gt_Gt_compare_complement_morphism;
-		  [ discriminate
-		    | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
-		      elim (ZL4 x); intros k E2; rewrite E2;
-			simpl in |- *; unfold gt, lt in |- *;
-			  apply le_n_S; apply le_plus_r ]
-		| assumption ]
-	    | rewrite (Pcompare_Eq_eq y z E0);
-          (* Case 3 *)
-	      elim (Pminus_mask_Gt (x + z) z);
-		[ intros t H; elim H; intros H1 H2; elim H2; intros H3 H4;
-		  unfold Pminus in |- *; rewrite H1; cut (x = t);
-		    [ intros E; rewrite E; auto with arith
-		      | apply Pplus_reg_r with (r := z); rewrite <- H3;
-			rewrite Pplus_comm; trivial with arith ]
-		  | pattern z at 1 in |- *; rewrite <- (Pcompare_Eq_eq y z E0);
-		    assumption ]
-	    | elim (Pminus_mask_Gt z y);
-	      [  (* Case 4 *)
-		intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
-		  unfold Pminus at 1 in |- *; rewrite H1; cut (x = k);
-		    [ intros E; rewrite E; rewrite (Pcompare_refl k);
-		      trivial with arith
-		      | apply Pplus_reg_r with (r := y); rewrite (Pplus_comm k y);
-			rewrite H3; apply Pcompare_Eq_eq; assumption ]
-		| apply ZC2; assumption ]
-	    | elim (Pminus_mask_Gt z y);
-	      [  (* Case 5 *)
-		intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
-		  unfold Pminus at 1 3 5 in |- *; rewrite H1;
-		    cut ((x ?= k)%positive Eq = Lt);
-		      [ intros E2; rewrite E2; elim (Pminus_mask_Gt k x);
-			[ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
-			  elim (Pminus_mask_Gt z (x + y));
-			    [ intros j H10; elim H10; intros H11 H12; elim H12;
-			      intros H13 H14; unfold Pminus in |- *;
-				rewrite H6; rewrite H11; cut (i = j);
-				  [ intros E; rewrite E; auto with arith
-				    | apply (Pplus_reg_l (x + y)); rewrite H13;
-				      rewrite (Pplus_comm x y); rewrite <- Pplus_assoc;
-					rewrite H8; assumption ]
-			      | apply ZC2; assumption ]
-			  | apply ZC2; assumption ]
-			| apply nat_of_P_lt_Lt_compare_complement_morphism;
-			  apply plus_lt_reg_l with (p := nat_of_P y);
-			    do 2 rewrite <- nat_of_P_plus_morphism;
-			      apply nat_of_P_lt_Lt_compare_morphism;
-				rewrite H3; rewrite Pplus_comm; assumption ]
-		| apply ZC2; assumption ]
-	    | elim (Pminus_mask_Gt z y);
-	      [  (* Case 6 *)
-		intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
-		  elim (Pminus_mask_Gt (x + y) z);
-		    [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
-		      unfold Pminus in |- *; rewrite H1; rewrite H6;
-			cut ((x ?= k)%positive Eq = Gt);
-			  [ intros H10; elim (Pminus_mask_Gt x k H10); intros j H11;
-			    elim H11; intros H12 H13; elim H13;
-			      intros H14 H15; rewrite H10; rewrite H12;
-				cut (i = j);
-				  [ intros H16; rewrite H16; auto with arith
-				    | apply (Pplus_reg_l (z + k)); rewrite <- (Pplus_assoc z k j);
-				      rewrite H14; rewrite (Pplus_comm z k);
-					rewrite <- Pplus_assoc; rewrite H8;
-					  rewrite (Pplus_comm x y); rewrite Pplus_assoc;
-					    rewrite (Pplus_comm k y); rewrite H3;
-					      trivial with arith ]
-			    | apply nat_of_P_gt_Gt_compare_complement_morphism;
-			      unfold lt, gt in |- *;
-				apply plus_lt_reg_l with (p := nat_of_P y);
-				  do 2 rewrite <- nat_of_P_plus_morphism;
-				    apply nat_of_P_lt_Lt_compare_morphism;
-				      rewrite H3; rewrite Pplus_comm; apply ZC1;
-					assumption ]
-		      | assumption ]
-		| apply ZC2; assumption ]
-	    | absurd ((x + y ?= z)%positive Eq = Eq);
-	      [  (* Case 7 *)
-		rewrite nat_of_P_gt_Gt_compare_complement_morphism;
-		  [ discriminate
-		    | rewrite nat_of_P_plus_morphism; unfold gt in |- *;
-		      apply lt_le_trans with (m := nat_of_P y);
-			[ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
-			  | apply le_plus_r ] ]
-		| assumption ]
-	    | absurd ((x + y ?= z)%positive Eq = Lt);
-	      [  (* Case 8 *)
-		rewrite nat_of_P_gt_Gt_compare_complement_morphism;
-		  [ discriminate
-		    | unfold gt in |- *; apply lt_le_trans with (m := nat_of_P y);
-		      [ exact (nat_of_P_gt_Gt_compare_morphism y z E0)
-			| rewrite nat_of_P_plus_morphism; apply le_plus_r ] ]
-		| assumption ]
-	    | elim Pminus_mask_Gt with (1 := E0); intros k H1;
-          (* Case 9 *)
-	      elim Pminus_mask_Gt with (1 := E1); intros i H2;
-		elim H1; intros H3 H4; elim H4; intros H5 H6;
-		  elim H2; intros H7 H8; elim H8; intros H9 H10;
-		    unfold Pminus in |- *; rewrite H3; rewrite H7;
-		      cut ((x + k)%positive = i);
-			[ intros E; rewrite E; auto with arith
-			  | apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc;
-			    rewrite H5; rewrite H9; rewrite Pplus_comm;
-			      trivial with arith ] ] ].
-Qed.
-
-Hint Local Resolve weak_assoc.
+ intros x y [|z|z]; simpl; trivial.
+ now rewrite Pplus_assoc.
+ case (Pcompare_spec y z); intros E0.
+ (* y = z *)
+ subst.
+ assert (H := Plt_plus_r z x). rewrite Pplus_comm in H. apply ZC2 in H.
+ now rewrite H, Pplus_minus_eq.
+ (* y < z *)
+ assert (Hz : (z = (z-y)+y)%positive).
+  rewrite Pplus_comm, Pplus_minus_lt; trivial.
+ pattern z at 4. rewrite Hz, Pplus_compare_mono_r.
+ case Pcompare_spec; intros E1; trivial; f_equal.
+ symmetry. rewrite Pplus_comm. apply Pminus_plus_distr.
+ rewrite Hz, Pplus_comm. now apply Pplus_lt_mono_r.
+ apply Pminus_minus_distr; trivial.
+ (* z < y *)
+ assert (LT : (z < x + y)%positive).
+  rewrite Pplus_comm. apply Plt_trans with y; trivial using Plt_plus_r.
+ apply ZC2 in LT. rewrite LT. f_equal.
+ now apply Pplus_minus_assoc.
+Qed.
 
 Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.
 Proof.
-  intros x y z; case x; case y; case z; auto with arith; intros;
-    [ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc;
-      rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc;
-	rewrite (Zplus_comm (Zpos p1)); trivial with arith
-      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
-	rewrite Zplus_comm; rewrite <- weak_assoc;
-	  rewrite (Zplus_comm (- Zpos p1));
-	    rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p);
-	      rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0));
-		trivial with arith
-      | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p));
-	rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0));
-	  trivial with arith
-      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
-	rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc;
-	  rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc;
-	    rewrite (Zplus_comm (Zpos p)); trivial with arith
-      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
-	apply weak_assoc
-      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
-	apply weak_assoc ].
+ intros [|x|x] [|y|y] [|z|z]; trivial.
+ apply weak_assoc.
+ apply weak_assoc.
+ now rewrite !Zplus_0_r.
+ rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc.
+  f_equal; apply Zplus_comm.
+ apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
+  rewrite 2 (Zplus_comm (-Zpos x)), 2 (Zplus_comm _ (Zpos z)).
+  now rewrite weak_assoc.
+ now rewrite !Zplus_0_r.
+ rewrite 2 (Zplus_comm (Zneg x)), 2 (Zplus_comm _ (Zpos z)).
+  now rewrite weak_assoc.
+ apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
+ rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc.
+  f_equal; apply Zplus_comm.
+ apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
+  apply weak_assoc.
+ apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
+  apply weak_assoc.
 Qed.
 
-
 Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).
 Proof.
-  intros; symmetry  in |- *; apply Zplus_assoc.
+  intros; symmetry ; apply Zplus_assoc.
 Qed.
 
 (** ** Associativity mixed with commutativity *)
@@ -498,7 +389,7 @@ Qed.
 Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
   intros n m p H; cut (- n + (n + m) = - n + (n + p));
     [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n);
-      rewrite Zplus_opp_r; simpl in |- *; trivial with arith
+      rewrite Zplus_opp_r; simpl; trivial with arith
       | rewrite H; trivial with arith ].
 Qed.
 
@@ -506,21 +397,21 @@ Qed.
 
 Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
 Proof.
-  intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y));
+  intros x y; unfold Zsucc; rewrite (Zplus_comm (x + y));
     rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1));
       trivial with arith.
 Qed.
 
 Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
 Proof.
-  intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
+  intros n m; unfold Zsucc; rewrite Zplus_assoc; trivial with arith.
 Qed.
 
 Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
 
 Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
 Proof.
-  unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
+  unfold Zsucc; intros n m; rewrite <- Zplus_assoc;
     rewrite (Zplus_comm (Zpos 1)); trivial with arith.
 Qed.
 
@@ -528,7 +419,7 @@ Qed.
 
 Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.
 Proof.
-  symmetry  in |- *; apply Zplus_0_r.
+  symmetry ; apply Zplus_0_r.
 Qed.
 
 Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.
@@ -561,7 +452,7 @@ Qed.
 Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.
 Proof.
   intros n; cut (Z0 <> Zpos 1);
-    [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n);
+    [ unfold not; intros H1 H2; apply H1; apply (Zplus_reg_l n);
       rewrite Zplus_0_r; exact H2
       | discriminate ].
 Qed.
@@ -569,7 +460,7 @@ Qed.
 Theorem Zpos_succ_morphism :
   forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).
 Proof.
-  intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *;
+  intro; rewrite Pplus_one_succ_r; unfold Zsucc; simpl;
     trivial with arith.
 Qed.
 
@@ -577,7 +468,7 @@ Qed.
 
 Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
 Proof.
-  intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
+  intros n; unfold Zsucc, Zpred; rewrite <- Zplus_assoc; simpl;
     rewrite Zplus_0_r; trivial with arith.
 Qed.
 
@@ -585,14 +476,14 @@ Hint Immediate Zsucc_pred: zarith.
 
 Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
 Proof.
-  intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
+  intros m; unfold Zpred, Zsucc; rewrite <- Zplus_assoc; simpl;
     rewrite Zplus_comm; auto with arith.
 Qed.
 
 Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.
 Proof.
   intros n m H.
-  change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *;
+  change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m);
     do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
       unfold Zsucc in H; rewrite H; trivial with arith.
 Qed.
@@ -640,10 +531,10 @@ Qed.
 
 Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.
 Proof.
-  intro x; destruct x; simpl in |- *.
+  intro x; destruct x; simpl.
   discriminate.
   injection; apply Psucc_discr.
-  destruct p; simpl in |- *.
+  destruct p; simpl.
     discriminate.
     intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
     discriminate.
@@ -658,7 +549,7 @@ Qed.
 
 Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.
 Proof.
-  unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
+  unfold not; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
 Qed.
 
 (**********************************************************************)
@@ -668,23 +559,23 @@ Qed.
 
 Lemma Zminus_0_r : forall n:Z, n - Z0 = n.
 Proof.
-  intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r;
+  intro; unfold Zminus; simpl; rewrite Zplus_0_r;
     trivial with arith.
 Qed.
 
 Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.
 Proof.
-  intro; symmetry  in |- *; apply Zminus_0_r.
+  intro; symmetry ; apply Zminus_0_r.
 Qed.
 
 Lemma Zminus_diag : forall n:Z, n - n = Z0.
 Proof.
-  intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith.
+  intro; unfold Zminus; rewrite Zplus_opp_r; trivial with arith.
 Qed.
 
 Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.
 Proof.
-  intro; symmetry  in |- *; apply Zminus_diag.
+  intro; symmetry ; apply Zminus_diag.
 Qed.
 
 
@@ -697,7 +588,7 @@ Qed.
 
 Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
 Proof.
-  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
+  intros n m; unfold Zminus, Zsucc; rewrite (Zplus_comm n (- m));
     rewrite <- Zplus_assoc; apply Zplus_comm.
 Qed.
 
@@ -708,7 +599,7 @@ Qed.
 
 Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
 Proof.
-  intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
+  intros n m p H; unfold Zminus; apply (Zplus_reg_l m);
     rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc;
       rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H;
 	trivial with arith.
@@ -716,32 +607,32 @@ Qed.
 
 Lemma Zminus_plus : forall n m:Z, n + m - n = m.
 Proof.
-  intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m);
+  intros n m; unfold Zminus; rewrite (Zplus_comm n m);
     rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r.
 Qed.
 
 Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.
 Proof.
-  unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
+  unfold Zminus; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
     apply Zplus_0_r.
 Qed.
 
 Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
 Proof.
-  intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
+  intros n m p; unfold Zminus; rewrite Zopp_plus_distr;
     rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p);
       rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith.
 Qed.
 
 Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).
 Proof.
-  intros; symmetry  in |- *; apply Zminus_plus_simpl_l.
+  intros; symmetry ; apply Zminus_plus_simpl_l.
 Qed.
 
 Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.
 Proof.
   intros x y n.
-  unfold Zminus in |- *.
+  unfold Zminus.
   rewrite Zopp_plus_distr.
   rewrite (Zplus_comm (- y) (- n)).
   rewrite Zplus_assoc.
@@ -765,7 +656,7 @@ Qed.
 
 Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
 Proof.
-  intros x y H; rewrite H; symmetry  in |- *; apply Zminus_diag_reverse.
+  intros x y H; rewrite H; symmetry ; apply Zminus_diag_reverse.
 Qed.
 
 Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
@@ -792,7 +683,7 @@ Qed.
 
 Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n.
 Proof.
-  intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity.
+  intro x; destruct x; simpl; try rewrite Pmult_1_r; reflexivity.
 Qed.
 
 (** ** Zero property of multiplication *)
@@ -818,7 +709,7 @@ Qed.
 
 Theorem Zmult_comm : forall n m:Z, n * m = m * n.
 Proof.
-  intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *;
+  intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl;
     try rewrite (Pmult_comm p q); reflexivity.
 Qed.
 
@@ -826,7 +717,7 @@ Qed.
 
 Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p.
 Proof.
-  intros x y z; destruct x; destruct y; destruct z; simpl in |- *;
+  intros x y z; destruct x; destruct y; destruct z; simpl;
     try rewrite Pmult_assoc; reflexivity.
 Qed.
 
@@ -856,7 +747,7 @@ Qed.
 
 Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0.
 Proof.
-  intros x y; destruct x; destruct y; auto; simpl in |- *; intro H;
+  intros x y; destruct x; destruct y; auto; simpl; intro H;
     discriminate H.
 Qed.
 
@@ -898,7 +789,7 @@ Qed.
 
 Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m).
 Proof.
-  intros x y; symmetry  in |- *; apply Zopp_mult_distr_l.
+  intros x y; symmetry ; apply Zopp_mult_distr_l.
 Qed.
 
 Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m.
@@ -922,34 +813,18 @@ Qed.
 Lemma weak_Zmult_plus_distr_r :
   forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m.
 Proof.
-  intros x y' z'; case y'; case z'; auto with arith; intros y z;
-    (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) ||
-      (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0;
-	[ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y));
-          trivial with arith
-	  | cut ((x * z ?= x * y)%positive Eq = Lt);
-            [ intros E; rewrite E; rewrite Pmult_minus_distr_l;
-              [ trivial with arith | apply ZC2; assumption ]
-              | apply nat_of_P_lt_Lt_compare_complement_morphism;
-		do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x);
-		  intros h H1; rewrite H1; apply mult_S_lt_compat_l;
-		    exact (nat_of_P_lt_Lt_compare_morphism z y E0) ]
-	  | cut ((x * z ?= x * y)%positive Eq = Gt);
-            [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith
-              | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;
-		do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x);
-		  intros h H1; rewrite H1; apply mult_S_lt_compat_l;
-		    exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]).
+ intros x [ |y|y] [ |z|z]; simpl; trivial; f_equal;
+  apply Pmult_plus_distr_l || rewrite Pmult_compare_mono_l;
+  case_eq ((y ?= z) Eq)%positive; intros H; trivial;
+   rewrite Pmult_minus_distr_l; trivial; now apply ZC1.
 Qed.
 
 Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p.
 Proof.
-  intros x y z; case x;
-    [ auto with arith
-      | intros x'; apply weak_Zmult_plus_distr_r
-      | intros p; apply Zopp_inj; rewrite Zopp_plus_distr;
-	do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg;
-	  apply weak_Zmult_plus_distr_r ].
+ intros [|x|x] y z. trivial.
+ apply weak_Zmult_plus_distr_r.
+ apply Zopp_inj; rewrite Zopp_plus_distr, !Zopp_mult_distr_l, !Zopp_neg.
+ apply weak_Zmult_plus_distr_r.
 Qed.
 
 Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p.
@@ -962,7 +837,7 @@ Qed.
 
 Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p.
 Proof.
-  intros x y z; unfold Zminus in |- *.
+  intros x y z; unfold Zminus.
   rewrite <- Zopp_mult_distr_l_reverse.
   apply Zmult_plus_distr_l.
 Qed.
@@ -1002,7 +877,7 @@ Qed.
 
 Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2.
 Proof.
-  intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x);
+  intros x; pattern x at 1 2; rewrite <- (Zmult_1_r x);
     rewrite <- Zmult_plus_distr_r; reflexivity.
 Qed.
 
@@ -1010,25 +885,25 @@ Qed.
 
 Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n.
 Proof.
-  intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r;
+  intros n m; unfold Zsucc; rewrite Zmult_plus_distr_r;
     rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l;
       trivial with arith.
 Qed.
 
 Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m.
 Proof.
-  intros; symmetry  in |- *; apply Zmult_succ_r.
+  intros; symmetry ; apply Zmult_succ_r.
 Qed.
 
 Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m.
 Proof.
-  intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l;
+  intros n m; unfold Zsucc; rewrite Zmult_plus_distr_l;
     rewrite Zmult_1_l; trivial with arith.
 Qed.
 
 Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m.
 Proof.
-  intros; symmetry  in |- *; apply Zmult_succ_l.
+  intros; symmetry; apply Zmult_succ_l.
 Qed.
 
 
@@ -1166,8 +1041,6 @@ Definition Z_of_nat (x:nat) :=
     | S y => Zpos (P_of_succ_nat y)
   end.
 
-Require Import BinNat.
-
 Definition Zabs_N (z:Z) :=
   match z with
     | Z0 => 0%N
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 4a401a2fe..a6a25541d 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -37,8 +37,8 @@ Lemma Z_of_nat_complete :
 Proof.
   intro x; destruct x; intros;
     [ exists 0%nat; auto with arith
-      | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros;
-	simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x);
+      | specialize (nat_of_P_is_S p); intros Hp; elim Hp; intros; exists (S x); intros;
+	simpl in |- *; specialize (nat_of_P_of_succ_nat x);
 	  intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos);
 	    apply nat_of_P_inj; auto with arith
       | absurd (0 <= Zneg p);
@@ -47,7 +47,7 @@ Proof.
 	  | assumption ] ].
 Qed.
 
-Lemma ZL4_inf : forall y:positive, {h : nat | nat_of_P y = S h}.
+Lemma nat_of_P_is_S_inf : forall y:positive, {h : nat | nat_of_P y = S h}.
 Proof.
   intro y; induction y as [p H| p H1| ];
     [ elim H; intros x H1; exists (S x + S x)%nat; unfold nat_of_P in |- *;
@@ -59,13 +59,15 @@ Proof.
       | exists 0%nat; auto with arith ].
 Qed.
 
+Notation ZL4_inf := nat_of_P_is_S_inf (only parsing).
+
 Lemma Z_of_nat_complete_inf :
  forall x:Z, 0 <= x -> {n : nat | x = Z_of_nat n}.
 Proof.
   intro x; destruct x; intros;
     [ exists 0%nat; auto with arith
-      | specialize (ZL4_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0);
-	intros; simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x0);
+      | specialize (nat_of_P_is_S_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0);
+	intros; simpl in |- *; specialize (nat_of_P_of_succ_nat x0);
 	  intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos);
 	    apply nat_of_P_inj; auto with arith
       | absurd (0 <= Zneg p);
@@ -127,20 +129,18 @@ Section Efficient_Rec.
 
   Let R_wf : well_founded R.
   Proof.
-    set
-      (f :=
-	fun z =>
+    set (f z :=
 	  match z with
 	    | Zpos p => nat_of_P p
 	    | Z0 => 0%nat
 	    | Zneg _ => 0%nat
-	  end) in *.
+	  end).
     apply well_founded_lt_compat with f.
-    unfold R, f in |- *; clear f R.
-    intros x y; case x; intros; elim H; clear H.
-    case y; intros; apply lt_O_nat_of_P || inversion H0.
-    case y; intros; apply nat_of_P_lt_Lt_compare_morphism || inversion H0; auto.
-    intros; elim H; auto.
+    unfold R, f; clear f R.
+    intros [|x|x] [|y|y] (H,H');
+     try (now elim H); try (discriminate H').
+    apply nat_of_P_pos.
+    now apply Plt_lt.
   Qed.
 
   Lemma natlike_rec2 :
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 8543652c6..a90b5bd69 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -125,7 +125,7 @@ Qed.
 Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
 Proof.
   destruct n; simpl; auto.
-  apply nat_of_P_o_P_of_succ_nat_eq_succ.
+  apply nat_of_P_of_succ_nat.
 Qed.
 
 Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat.
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 5e7441462..10f07a864 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -13,32 +13,26 @@
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France)            *)
 (**********************************************************************)
 
-Require Export BinPos.
-Require Export BinInt.
-Require Import Lt.
-Require Import Gt.
-Require Import Plus.
-Require Import Mult.
+Require Export BinPos BinInt.
+Require Import Lt Gt Plus Mult.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (***************************)
 (** * Comparison on integers *)
 
 Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq.
 Proof.
-  intro x; destruct x as [| p| p]; simpl in |- *;
-    [ reflexivity | apply Pcompare_refl | rewrite Pcompare_refl; reflexivity ].
+ destruct n as [|p|p]; simpl; trivial.
+ apply Pcompare_refl.
+ apply CompOpp_iff, Pcompare_refl.
 Qed.
 
 Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m.
 Proof.
-  intros x y; destruct x as [| x'| x']; destruct y as [| y'| y']; simpl in |- *;
-    intro H; reflexivity || (try discriminate H);
-      [ rewrite (Pcompare_Eq_eq x' y' H); reflexivity
-	| rewrite (Pcompare_Eq_eq x' y');
-	  [ reflexivity
-	    | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ].
+ intros [|x|x] [|y|y] H; simpl in *; try easy; f_equal.
+  now apply Pcompare_Eq_eq.
+  apply CompOpp_iff in H. now apply Pcompare_Eq_eq.
 Qed.
 
 Ltac destr_zcompare :=
@@ -52,45 +46,40 @@ Ltac destr_zcompare :=
 
 Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m.
 Proof.
-  intros x y; split; intro E;
-    [ apply Zcompare_Eq_eq; assumption | rewrite E; apply Zcompare_refl ].
+ intros x y; split; intro E; subst.
+ now apply Zcompare_Eq_eq. now apply Zcompare_refl.
 Qed.
 
 Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n).
 Proof.
-  intros x y; destruct x; destruct y; simpl in |- *;
-    reflexivity || discriminate H || rewrite Pcompare_antisym;
-      reflexivity.
+ intros [|x|x] [|y|y]; simpl; try easy; f_equal; apply Pcompare_antisym.
 Qed.
 
-Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
+Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).
 Proof.
-  intros x y.
-  rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt).
-  split.
-  auto using CompOpp_inj.
-  intros; f_equal; auto.
+ intros.
+ destruct (n?=m) as [ ]_eqn:H; constructor; trivial.
+ now apply Zcompare_Eq_eq.
+ red; now rewrite <- Zcompare_antisym, H.
 Qed.
 
-Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).
+Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
 Proof.
-  intros.
-  destruct (n?=m) as [ ]_eqn:H; constructor; auto.
-  apply Zcompare_Eq_eq; auto.
-  red; rewrite <- Zcompare_antisym, H; auto.
+ intros x y.
+ rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt).
+ split.
+ auto using CompOpp_inj.
+ intros; f_equal; auto.
 Qed.
 
-
 (** * Transitivity of comparison *)
 
 Lemma Zcompare_Lt_trans :
   forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt.
 Proof.
-  intros x y z; case x; case y; case z; simpl;
-    try discriminate; auto with arith.
-  intros; eapply Plt_trans; eauto.
-  intros p q r; rewrite 3 Pcompare_antisym; simpl.
-  intros; eapply Plt_trans; eauto.
+ intros n m p; destruct n,m,p; simpl; try discriminate; trivial.
+ eapply Plt_trans; eauto.
+ rewrite 3 Pcompare_antisym; simpl. intros; eapply Plt_trans; eauto.
 Qed.
 
 Lemma Zcompare_Gt_trans :
@@ -107,281 +96,105 @@ Qed.
 
 Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n).
 Proof.
-  intros x y; case x; case y; simpl in |- *; auto with arith; intros;
-    rewrite <- ZC4; trivial with arith.
+ destruct n, m; simpl; trivial; intros; now rewrite <- ZC4.
 Qed.
 
-Hint Local Resolve Pcompare_refl.
-
 (** * Comparison first-order specification *)
 
 Lemma Zcompare_Gt_spec :
-  forall n m:Z, (n ?= m) = Gt ->  exists h : positive, n + - m = Zpos h.
-Proof.
-  intros x y; case x; case y;
-    [ simpl in |- *; intros H; discriminate H
-      | simpl in |- *; intros p H; discriminate H
-      | intros p H; exists p; simpl in |- *; auto with arith
-      | intros p H; exists p; simpl in |- *; auto with arith
-      | intros q p H; exists (p - q)%positive; unfold Zplus, Zopp in |- *;
-	unfold Zcompare in H; rewrite H; trivial with arith
-      | intros q p H; exists (p + q)%positive; simpl in |- *; trivial with arith
-      | simpl in |- *; intros p H; discriminate H
-      | simpl in |- *; intros q p H; discriminate H
-      | unfold Zcompare in |- *; intros q p; rewrite <- ZC4; intros H;
-	exists (q - p)%positive; simpl in |- *; rewrite (ZC1 q p H);
-	  trivial with arith ].
+  forall n m:Z, (n ?= m) = Gt ->  exists h, n + - m = Zpos h.
+Proof.
+ intros [|p|p] [|q|q]; simpl; try discriminate.
+ now exists q.
+ now exists p.
+ intros GT. exists (p-q)%positive. now rewrite GT.
+ now exists (p+q)%positive.
+ intros LT. apply CompOpp_iff in LT. simpl in LT.
+ exists (q-p)%positive. now rewrite LT.
 Qed.
 
 (** * Comparison and addition *)
 
-Lemma weaken_Zcompare_Zplus_compatible :
-  (forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m)) ->
-  forall n m p:Z, (p + n ?= p + m) = (n ?= m).
-Proof.
-  intros H x y z; destruct z;
-    [ reflexivity
-      | apply H
-      | rewrite (Zcompare_opp x y); rewrite Zcompare_opp;
-	do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg;
-	  apply H ].
-Qed.
-
-Hint Local Resolve ZC4.
+Local Hint Resolve Pcompare_refl.
 
-Lemma weak_Zcompare_Zplus_compatible :
+Lemma weak_Zcompare_plus_compat :
   forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m).
 Proof.
-  intros x y z; case x; case y; simpl in |- *; auto with arith;
-    [ intros p; apply nat_of_P_lt_Lt_compare_complement_morphism; apply ZL17
-      | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;
-	apply nat_of_P_gt_Gt_compare_complement_morphism;
-	  rewrite nat_of_P_minus_morphism;
-	    [ unfold gt in |- *; apply ZL16 | assumption ]
-      | intros p; ElimPcompare z p; intros E; auto with arith;
-	apply nat_of_P_gt_Gt_compare_complement_morphism;
-	  unfold gt in |- *; apply ZL17
-      | intros p q; ElimPcompare q p; intros E; rewrite E;
-	[ rewrite (Pcompare_Eq_eq q p E); apply Pcompare_refl
-	  | apply nat_of_P_lt_Lt_compare_complement_morphism;
-	    do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;
-	      apply nat_of_P_lt_Lt_compare_morphism with (1 := E)
-	  | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;
-	    do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;
-	      exact (nat_of_P_gt_Gt_compare_morphism q p E) ]
-      | intros p q; ElimPcompare z p; intros E; rewrite E; auto with arith;
-	apply nat_of_P_gt_Gt_compare_complement_morphism;
-	  rewrite nat_of_P_minus_morphism;
-	    [ unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
-	      [ apply ZL16 | apply ZL17 ]
-	      | assumption ]
-      | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;
-	simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
-	  rewrite nat_of_P_minus_morphism; [ apply ZL16 | assumption ]
-      | intros p q; ElimPcompare z q; intros E; rewrite E; auto with arith;
-	simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
-	  rewrite nat_of_P_minus_morphism;
-	    [ apply lt_trans with (m := nat_of_P z); [ apply ZL16 | apply ZL17 ]
-	      | assumption ]
-      | intros p q; ElimPcompare z q; intros E0; rewrite E0; ElimPcompare z p;
-	intros E1; rewrite E1; ElimPcompare q p; intros E2;
-	  rewrite E2; auto with arith;
-	    [ absurd ((q ?= p)%positive Eq = Lt);
-	      [ rewrite <- (Pcompare_Eq_eq z q E0);
-		rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z);
-		  discriminate
-		| assumption ]
-	      | absurd ((q ?= p)%positive Eq = Gt);
-		[ rewrite <- (Pcompare_Eq_eq z q E0);
-		  rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z);
-		    discriminate
-		  | assumption ]
-	      | absurd ((z ?= p)%positive Eq = Lt);
-		[ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2);
-		  rewrite (Pcompare_refl q); discriminate
-		  | assumption ]
-	      | absurd ((z ?= p)%positive Eq = Lt);
-		[ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate
-		  | assumption ]
-	      | absurd ((z ?= p)%positive Eq = Gt);
-		[ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2);
-		  rewrite (Pcompare_refl q); discriminate
-		  | assumption ]
-	      | absurd ((z ?= p)%positive Eq = Gt);
-		[ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate
-		  | assumption ]
-	      | absurd ((z ?= q)%positive Eq = Lt);
-		[ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2);
-		  rewrite (Pcompare_refl p); discriminate
-		  | assumption ]
-	      | absurd ((p ?= q)%positive Eq = Gt);
-		[ rewrite <- (Pcompare_Eq_eq z p E1); rewrite E0; discriminate
-		  | apply ZC2; assumption ]
-	      | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2);
-		rewrite (Pcompare_refl (p - z)); auto with arith
-	      | simpl in |- *; rewrite <- ZC4;
-		apply nat_of_P_gt_Gt_compare_complement_morphism;
-		  rewrite nat_of_P_minus_morphism;
-		    [ rewrite nat_of_P_minus_morphism;
-		      [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);
-			rewrite le_plus_minus_r;
-			  [ rewrite le_plus_minus_r;
-			    [ apply nat_of_P_lt_Lt_compare_morphism; assumption
-			      | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-				assumption ]
-			    | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-			      assumption ]
-			| apply ZC2; assumption ]
-		      | apply ZC2; assumption ]
-	      | simpl in |- *; rewrite <- ZC4;
-		apply nat_of_P_lt_Lt_compare_complement_morphism;
-		  rewrite nat_of_P_minus_morphism;
-		    [ rewrite nat_of_P_minus_morphism;
-		      [ apply plus_lt_reg_l with (p := nat_of_P z);
-			rewrite le_plus_minus_r;
-			  [ rewrite le_plus_minus_r;
-			    [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
-			      assumption
-			      | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-				assumption ]
-			    | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-			      assumption ]
-			| apply ZC2; assumption ]
-		      | apply ZC2; assumption ]
-	      | absurd ((z ?= q)%positive Eq = Lt);
-		[ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate
-		  | assumption ]
-	      | absurd ((q ?= p)%positive Eq = Lt);
-		[ cut ((q ?= p)%positive Eq = Gt);
-		  [ intros E; rewrite E; discriminate
-		    | apply nat_of_P_gt_Gt_compare_complement_morphism;
-		      unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
-			[ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
-			  | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]
-		  | assumption ]
-	      | absurd ((z ?= q)%positive Eq = Gt);
-		[ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2);
-		  rewrite (Pcompare_refl p); discriminate
-		  | assumption ]
-	      | absurd ((z ?= q)%positive Eq = Gt);
-		[ rewrite (Pcompare_Eq_eq z p E1); rewrite ZC1;
-		  [ discriminate | assumption ]
-		  | assumption ]
-	      | absurd ((z ?= q)%positive Eq = Gt);
-		[ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate
-		  | assumption ]
-	      | absurd ((q ?= p)%positive Eq = Gt);
-		[ rewrite ZC1;
-		  [ discriminate
-		    | apply nat_of_P_gt_Gt_compare_complement_morphism;
-		      unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
-			[ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
-			  | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]
-		  | assumption ]
-	      | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); apply Pcompare_refl
-	      | simpl in |- *; apply nat_of_P_gt_Gt_compare_complement_morphism;
-		unfold gt in |- *; rewrite nat_of_P_minus_morphism;
-		  [ rewrite nat_of_P_minus_morphism;
-		    [ apply plus_lt_reg_l with (p := nat_of_P p);
-		      rewrite le_plus_minus_r;
-			[ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P q);
-			  rewrite plus_assoc; rewrite le_plus_minus_r;
-			    [ rewrite (plus_comm (nat_of_P q)); apply plus_lt_compat_l;
-			      apply nat_of_P_lt_Lt_compare_morphism;
-				assumption
-			      | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-				apply ZC1; assumption ]
-			  | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-			    apply ZC1; assumption ]
-		      | assumption ]
-		    | assumption ]
-	      | simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
-		rewrite nat_of_P_minus_morphism;
-		  [ rewrite nat_of_P_minus_morphism;
-		    [ apply plus_lt_reg_l with (p := nat_of_P q);
-		      rewrite le_plus_minus_r;
-			[ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
-			  rewrite plus_assoc; rewrite le_plus_minus_r;
-			    [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
-			      apply nat_of_P_lt_Lt_compare_morphism;
-				apply ZC1; assumption
-			      | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-				apply ZC1; assumption ]
-			  | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-			    apply ZC1; assumption ]
-		      | assumption ]
-		    | assumption ] ] ].
+ intros [|x|x] [|y|y] z; simpl; trivial; try apply ZC2;
+  try apply Plt_plus_r.
+ case Pcompare_spec; intros E0; trivial; try apply ZC2;
+  now apply Pminus_decr.
+ apply Pplus_compare_mono_l.
+ case Pcompare_spec; intros E0; trivial; try apply ZC2.
+  apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r.
+ case Pcompare_spec; intros E0; trivial; try apply ZC2.
+  now apply Pminus_decr.
+ case Pcompare_spec; intros E0; trivial; try apply ZC2.
+  apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r.
+ case Pcompare_spec; intros E0; simpl; subst.
+  now case Pcompare_spec.
+  case Pcompare_spec; intros E1; simpl; subst; trivial.
+  now rewrite <- ZC4.
+  f_equal.
+  apply Pminus_compare_mono_r; trivial.
+  rewrite <- ZC4. symmetry. now apply Plt_trans with z.
+  case Pcompare_spec; intros E1; simpl; subst; trivial.
+  now rewrite E0.
+  symmetry. apply CompOpp_iff. now apply Plt_trans with z.
+  rewrite <- ZC4.
+  apply Pminus_compare_mono_l; trivial.
 Qed.
 
 Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m).
 Proof.
-  exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible).
+ intros x y [|z|z]; trivial.
+ apply weak_Zcompare_plus_compat.
+ rewrite (Zcompare_opp x y), Zcompare_opp, 2 Zopp_plus_distr, Zopp_neg.
+ apply weak_Zcompare_plus_compat.
 Qed.
 
 Lemma Zplus_compare_compat :
   forall (r:comparison) (n m p q:Z),
     (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
 Proof.
-  intros r x y z t; case r;
-    [ intros H1 H2; elim (Zcompare_Eq_iff_eq x y); elim (Zcompare_Eq_iff_eq z t);
-      intros H3 H4 H5 H6; rewrite H3;
-	[ rewrite H5;
-	  [ elim (Zcompare_Eq_iff_eq (y + t) (y + t)); auto with arith
-	    | auto with arith ]
-	  | auto with arith ]
-      | intros H1 H2; elim (Zcompare_Gt_Lt_antisym (y + t) (x + z)); intros H3 H4;
-	apply H3; apply Zcompare_Gt_trans with (m := y + z);
-	  [ rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym t z);
-	    auto with arith
-	    | do 2 rewrite <- (Zplus_comm z); rewrite Zcompare_plus_compat;
-	      elim (Zcompare_Gt_Lt_antisym y x); auto with arith ]
-      | intros H1 H2; apply Zcompare_Gt_trans with (m := x + t);
-	[ rewrite Zcompare_plus_compat; assumption
-	  | do 2 rewrite <- (Zplus_comm t); rewrite Zcompare_plus_compat;
-	    assumption ] ].
+ intros [ | | ] x y z t H H'.
+ apply Zcompare_Eq_eq in H. apply Zcompare_Eq_eq in H'. subst.
+  apply Zcompare_refl.
+ apply Zcompare_Lt_trans with (y+z).
+ now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat.
+ now rewrite Zcompare_plus_compat.
+ apply Zcompare_Gt_trans with (y+z).
+ now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat.
+ now rewrite Zcompare_plus_compat.
 Qed.
 
 Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt.
 Proof.
-  intro x; unfold Zsucc in |- *; pattern x at 2 in |- *;
-    rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat;
-      reflexivity.
-Qed.
-
-Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m + 1) <> Lt.
-Proof.
-  intros x y; split;
-    [ intro H; elim_compare x (y + 1);
-      [ intro H1; rewrite H1; discriminate
-	| intros H1; elim Zcompare_Gt_spec with (1 := H); intros h H2;
-	  absurd ((nat_of_P h > 0)%nat /\ (nat_of_P h < 1)%nat);
-	    [ unfold not in |- *; intros H3; elim H3; intros H4 H5;
-              absurd (nat_of_P h > 0)%nat;
-		[ unfold gt in |- *; apply le_not_lt; apply le_S_n; exact H5
-		  | assumption ]
-	      | split;
-		[ elim (ZL4 h); intros i H3; rewrite H3; apply gt_Sn_O
-		  | change (nat_of_P h < nat_of_P 1)%nat in |- *;
-		    apply nat_of_P_lt_Lt_compare_morphism;
-		      change ((Zpos h ?= 1) = Lt) in |- *; rewrite <- H2;
-			rewrite <- (fun m n:Z => Zcompare_plus_compat m n y);
-			  rewrite (Zplus_comm x); rewrite Zplus_assoc;
-			    rewrite Zplus_opp_r; simpl in |- *; exact H1 ] ]
-	| intros H1; rewrite H1; discriminate ]
-      | intros H; elim_compare x (y + 1);
-	[ intros H1; elim (Zcompare_Eq_iff_eq x (y + 1)); intros H2 H3;
-	  rewrite (H2 H1); exact (Zcompare_succ_Gt y)
-	  | intros H1; absurd ((x ?= y + 1) = Lt); assumption
-	  | intros H1; apply Zcompare_Gt_trans with (m := Zsucc y);
-	    [ exact H1 | exact (Zcompare_succ_Gt y) ] ] ].
+ intro x; unfold Zsucc; pattern x at 2; rewrite <- (Zplus_0_r x);
+  now rewrite Zcompare_plus_compat.
+Qed.
+
+Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m+1) <> Lt.
+Proof.
+ intros x y; split; intros H.
+ (* -> *)
+ destruct (Zcompare_Gt_spec _ _ H) as (h,EQ).
+ replace x with (y+Zpos h) by (rewrite <- EQ; apply Zplus_minus).
+ rewrite Zcompare_plus_compat. apply Plt_1.
+ (* <- *)
+ assert (H' := Zcompare_succ_Gt y).
+ destruct (Zcompare_spec x (y+1)) as [->|LT|GT]; trivial.
+  now elim H.
+  apply Zcompare_Gt_Lt_antisym in GT.
+   apply Zcompare_Gt_trans with (y+1); trivial.
 Qed.
 
 (** * Successor and comparison *)
 
 Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m).
 Proof.
-  intros n m; unfold Zsucc in |- *; do 2 rewrite (fun t:Z => Zplus_comm t 1);
-    rewrite Zcompare_plus_compat; auto with arith.
+ intros n m; unfold Zsucc;
+  now rewrite 2 (Zplus_comm _ 1), Zcompare_plus_compat.
 Qed.
 
 (** * Multiplication and comparison *)
@@ -389,28 +202,13 @@ Qed.
 Lemma Zcompare_mult_compat :
   forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m).
 Proof.
-  intros x; induction x as [p H| p H| ];
-    [ intros y z; cut (Zpos (xI p) = Zpos p + Zpos p + 1);
-      [ intros E; rewrite E; do 4 rewrite Zmult_plus_distr_l;
-	do 2 rewrite Zmult_1_l; apply Zplus_compare_compat;
-	  [ apply Zplus_compare_compat; apply H | trivial with arith ]
-	| simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]
-      | intros y z; cut (Zpos (xO p) = Zpos p + Zpos p);
-	[ intros E; rewrite E; do 2 rewrite Zmult_plus_distr_l;
-	  apply Zplus_compare_compat; apply H
-	  | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]
-      | intros y z; do 2 rewrite Zmult_1_l; trivial with arith ].
+ intros p [|n|n] [|m|m]; simpl; trivial.
+  apply Pmult_compare_mono_l.
+  f_equal. apply Pmult_compare_mono_l.
 Qed.
 
-
 (** * Reverting [x ?= y] to trichotomy *)
 
-Lemma rename :
-  forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x.
-Proof.
-  auto with arith.
-Qed.
-
 Lemma Zcompare_elim :
   forall (c1 c2 c3:Prop) (n m:Z),
     (n = m -> c1) ->
@@ -421,11 +219,9 @@ Lemma Zcompare_elim :
                        | Gt => c3
                      end.
 Proof.
-  intros c1 c2 c3 x y; intros.
-  apply rename with (x := x ?= y); intro r; elim r;
-    [ intro; apply H; apply (Zcompare_Eq_eq x y); assumption
-      | unfold Zlt in H0; assumption
-      | unfold Zgt in H1; assumption ].
+ intros c1 c2 c3 x y EQ LT GT; intros.
+ case Zcompare_spec; auto.
+ intro H. apply GT. red. now rewrite <- Zcompare_antisym, H.
 Qed.
 
 Lemma Zcompare_eq_case :
@@ -450,8 +246,8 @@ Lemma Zcompare_egal_dec :
     (n > m -> p > q) -> (n ?= m) = (p ?= q).
 Proof.
   intros x1 y1 x2 y2.
-  unfold Zgt in |- *; unfold Zlt in |- *; case (x1 ?= y1); case (x2 ?= y2);
-    auto with arith; symmetry  in |- *; auto with arith.
+  unfold Zgt; unfold Zlt; case (x1 ?= y1); case (x2 ?= y2);
+    auto with arith; symmetry; auto with arith.
 Qed.
 
 (** * Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *)
@@ -464,7 +260,7 @@ Lemma Zle_compare :
 		| Gt => False
               end.
 Proof.
-  intros x y; unfold Zle in |- *; elim (x ?= y); auto with arith.
+  intros x y; unfold Zle; elim (x ?= y); auto with arith.
 Qed.
 
 Lemma Zlt_compare :
@@ -487,7 +283,7 @@ Lemma Zge_compare :
 		| Gt => True
               end.
 Proof.
-  intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith.
+  intros x y; unfold Zge; elim (x ?= y); auto.
 Qed.
 
 Lemma Zgt_compare :
@@ -498,8 +294,7 @@ Lemma Zgt_compare :
                | Gt => True
              end.
 Proof.
-  intros x y; unfold Zgt in |- *; elim (x ?= y); intros;
-    discriminate || trivial with arith.
+  intros x y; unfold Zgt; now elim (x ?= y).
 Qed.
 
 (*********************)
@@ -517,7 +312,7 @@ Qed.
 Lemma Zmult_compare_compat_r :
   forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p).
 Proof.
-  intros x y z H; rewrite (Zmult_comm x z); rewrite (Zmult_comm y z);
+  intros x y z H; rewrite 2 (Zmult_comm _ z);
     apply Zmult_compare_compat_l; assumption.
 Qed.
 
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
index 0e71bb4c3..a45d433c8 100644
--- a/theories/ZArith/Zdiv_def.v
+++ b/theories/ZArith/Zdiv_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Nnat Ndiv_def.
+Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Znat Ndiv_def.
 Local Open Scope Z_scope.
 
 (** * Definitions of divisions for binary integers *)
diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v
index 588b33037..44983f691 100644
--- a/theories/ZArith/Zlog_def.v
+++ b/theories/ZArith/Zlog_def.v
@@ -12,55 +12,27 @@ Local Open Scope Z_scope.
 
 (** Definition of Zlog2 *)
 
-Fixpoint Plog2_Z (p:positive) : Z :=
-  match p with
-    | 1 => Z0
-    | p~0 => Zsucc (Plog2_Z p)
-    | p~1 => Zsucc (Plog2_Z p)
-  end%positive.
-
 Definition Zlog2 z :=
   match z with
-    | Zpos p => Plog2_Z p
+    | Zpos (p~1) => Zpos (Psize_pos p)
+    | Zpos (p~0) => Zpos (Psize_pos p)
     | _ => 0
   end.
 
-Lemma Plog2_Z_nonneg : forall p, 0 <= Plog2_Z p.
-Proof.
- induction p; simpl; auto with zarith.
-Qed.
-
-Lemma Plog2_Z_spec : forall p,
- 2^(Plog2_Z p) <= Zpos p < 2^(Zsucc (Plog2_Z p)).
-Proof.
- induction p; simpl;
-  try rewrite 2 Zpower_succ_r; auto using Plog2_Z_nonneg with zarith.
- (* p~1 *)
- change (Zpos p~1) with (Zsucc (2 * Zpos p)).
- split; destruct IHp as [LE LT].
- apply Zle_trans with (2 * Zpos p).
- now apply Zmult_le_compat_l.
- apply Zle_succ.
- apply Zle_succ_l. apply Zle_succ_l in LT.
- replace (Zsucc (Zsucc (2 * Zpos p))) with (2 * (Zsucc (Zpos p))).
- now apply Zmult_le_compat_l.
- simpl. now rewrite Pplus_one_succ_r.
- (* p~0 *)
- change (Zpos p~0) with (2 * Zpos p).
- split; destruct IHp.
- now apply Zmult_le_compat_l.
- now apply Zmult_lt_compat_l.
- (* 1 *)
- now split.
-Qed.
-
 Lemma Zlog2_spec : forall n, 0 < n ->
  2^(Zlog2 n) <= n < 2^(Zsucc (Zlog2 n)).
 Proof.
- intros [|p|p] Hn; try discriminate. apply Plog2_Z_spec.
+ intros [|[p|p|]|] Hn; split; try easy; unfold Zlog2;
+  rewrite <- ?Zpos_succ_morphism, Zpower_Ppow.
+ eapply Zle_trans with (Zpos (p~0)).
+ apply Psize_pos_le.
+ apply Zlt_le_weak. exact (Pcompare_p_Sp (p~0)).
+ apply Psize_pos_gt.
+ apply Psize_pos_le.
+ apply Psize_pos_gt.
 Qed.
 
 Lemma Zlog2_nonpos : forall n, n<=0 -> Zlog2 n = 0.
 Proof.
- intros [|p|p] Hn. reflexivity. now destruct Hn. reflexivity.
+ intros [|p|p] H; trivial; now destruct H.
 Qed.
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index ddb1eed9f..b80e96c2a 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -7,9 +7,12 @@
 (************************************************************************)
 
 (**********************************************************************)
+
 (** The integer logarithms with base 2.
 
-    There are three logarithms,
+    NOTA: This file is deprecated, please use Zlog2 defined in Zlog_def.
+
+    There are three logarithms defined here,
     depending on the rounding of the real 2-based logarithm:
     - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)]
       i.e. [Log_inf x] is the biggest integer that is smaller than [Log x]
@@ -25,9 +28,12 @@ Section Log_pos. (* Log of positive integers *)
 
   (** First we build [log_inf] and [log_sup] *)
 
-  (** [log_inf] is exactly the same as the new [Plog2_Z] *)
-
-  Definition log_inf : positive -> Z := Eval red in Plog2_Z.
+  Fixpoint log_inf (p:positive) : Z :=
+    match p with
+      | xH => 0 (* 1 *)
+      | xO q => Zsucc (log_inf q)       (* 2n *)
+      | xI q => Zsucc (log_inf q)       (* 2n+1 *)
+    end.
 
   Fixpoint log_sup (p:positive) : Z :=
     match p with
@@ -38,8 +44,15 @@ Section Log_pos. (* Log of positive integers *)
 
   Hint Unfold log_inf log_sup.
 
+  Lemma Psize_log_inf : forall p, Zpos (Psize_pos p) = Zsucc (log_inf p).
+  Proof.
+   induction p; simpl; now rewrite ?Zpos_succ_morphism, ?IHp.
+  Qed.
+
   Lemma Zlog2_log_inf : forall p, Zlog2 (Zpos p) = log_inf p.
-  Proof. reflexivity. Qed.
+  Proof.
+   unfold Zlog2. destruct p; simpl; trivial; apply Psize_log_inf.
+  Qed.
 
   Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p.
   Proof.
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index b4bd470ab..f6b038cbd 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -18,13 +18,6 @@ Open Local Scope Z_scope.
 
 (** [n]th iteration of the function [f] *)
 
-Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A :=
-  match n with
-    | xH => f x
-    | xO n' => iter_pos n' A f (iter_pos n' A f x)
-    | xI n' => f (iter_pos n' A f (iter_pos n' A f x))
-  end.
-
 Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
   match n with
     | Z0 => x
@@ -32,58 +25,9 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
     | Zneg p => x
   end.
 
-Theorem iter_nat_of_P :
-  forall (p:positive) (A:Type) (f:A -> A) (x:A),
-    iter_pos p A f x = iter_nat (nat_of_P p) A f x.
-Proof.
-  intro n; induction n as [p H| p H| ];
-    [ intros; simpl in |- *; rewrite (H A f x);
-      rewrite (H A f (iter_nat (nat_of_P p) A f x));
-	rewrite (ZL6 p); symmetry  in |- *; apply f_equal with (f := f);
-	  apply iter_nat_plus
-      | intros; unfold nat_of_P in |- *; simpl in |- *; rewrite (H A f x);
-	rewrite (H A f (iter_nat (nat_of_P p) A f x));
-	  rewrite (ZL6 p); symmetry  in |- *; apply iter_nat_plus
-      | simpl in |- *; auto with arith ].
-Qed.
-
 Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
   iter n A f x = iter_nat (Zabs_nat n) A f x.
 intros n A f x; case n; auto.
 intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P.
 intros p abs; case abs; trivial.
 Qed.
-
-Theorem iter_pos_plus :
-  forall (p q:positive) (A:Type) (f:A -> A) (x:A),
-    iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).
-Proof.
-  intros n m; intros.
-  rewrite (iter_nat_of_P m A f x).
-  rewrite (iter_nat_of_P n A f (iter_nat (nat_of_P m) A f x)).
-  rewrite (iter_nat_of_P (n + m) A f x).
-  rewrite (nat_of_P_plus_morphism n m).
-  apply iter_nat_plus.
-Qed.
-
-(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv],
-    then the iterates of [f] also preserve it. *)
-
-Theorem iter_nat_invariant :
-  forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
-    (forall x:A, Inv x -> Inv (f x)) ->
-    forall x:A, Inv x -> Inv (iter_nat n A f x).
-Proof.
-  simple induction n; intros;
-    [ trivial with arith
-      | simpl in |- *; apply H0 with (x := iter_nat n0 A f x); apply H;
-	trivial with arith ].
-Qed.
-
-Theorem iter_pos_invariant :
-  forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
-    (forall x:A, Inv x -> Inv (f x)) ->
-    forall x:A, Inv x -> Inv (iter_pos p A f x).
-Proof.
-  intros; rewrite iter_nat_of_P; apply iter_nat_invariant; trivial with arith.
-Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index c7e6d5750..5f4a6e38d 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -10,14 +10,8 @@
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
-Require Import BinPos.
-Require Import BinInt.
-Require Import Zcompare.
-Require Import Zorder.
-Require Import Decidable.
-Require Import Peano_dec.
-Require Import Min Max.
-Require Export Compare_dec.
+Require Import BinPos BinInt BinNat Zcompare Zorder.
+Require Import Decidable Peano_dec Min Max Compare_dec.
 
 Open Local Scope Z_scope.
 
@@ -26,46 +20,49 @@ Definition neq (x y:nat) := x <> y.
 (************************************************)
 (** Properties of the injection from nat into Z *)
 
+Lemma Zpos_P_of_succ_nat : forall n:nat,
+ Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Proof.
+  intros [|n]. trivial. apply Zpos_succ_morphism.
+Qed.
+
 (** Injection and successor *)
 
-Theorem inj_0 : Z_of_nat 0 = 0%Z.
+Theorem inj_0 : Z_of_nat 0 = 0.
 Proof.
   reflexivity.
 Qed.
 
 Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
-  intro y; induction y as [| n H];
-    [ unfold Zsucc in |- *; simpl in |- *; trivial with arith
-      | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
-	rewrite Zpos_succ_morphism; trivial with arith ].
+  exact Zpos_P_of_succ_nat.
+Qed.
+
+(** Injection and comparison *)
+
+Theorem inj_compare : forall n m:nat,
+ (Z_of_nat n ?= Z_of_nat m) = nat_compare n m.
+Proof.
+ induction n; destruct m; trivial.
+ rewrite 2 inj_S, Zcompare_succ_compat. now simpl.
 Qed.
 
 (** Injection and equality. *)
 
 Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-  intros x y H; rewrite H; trivial with arith.
+  intros; subst; trivial.
 Qed.
 
-Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
+Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
 Proof.
-  unfold neq, Zne, not in |- *; intros x y H1 H2; apply H1; generalize H2;
-    case x; case y; intros;
-      [ auto with arith
-	| discriminate H0
-	| discriminate H0
-	| simpl in H0; injection H0;
-	  do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ;
-	    intros E; rewrite E; auto with arith ].
+  intros n m H. apply nat_compare_eq.
+  now rewrite <- inj_compare, H, Zcompare_refl.
 Qed.
 
-Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
 Proof.
-  intros x y H.
-  destruct (eq_nat_dec x y) as [H'|H']; auto.
-  exfalso.
-  exact (inj_neq _ _ H' H).
+  unfold neq, Zne. intros n m H. contradict H. now apply inj_eq_rev.
 Qed.
 
 Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
@@ -73,17 +70,9 @@ Proof.
  split; [apply inj_eq | apply inj_eq_rev].
 Qed.
 
+(** Injection and order *)
 
-(** Injection and order relations: *)
-
-Theorem inj_compare : forall n m:nat,
- (Z_of_nat n ?= Z_of_nat m) = nat_compare n m.
-Proof.
- induction n; destruct m; trivial.
- rewrite 2 inj_S, Zcompare_succ_compat. now simpl.
-Qed.
-
-(* Both ways ... *)
+(** Both ways ... *)
 
 Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
 Proof.
@@ -137,50 +126,43 @@ Proof. apply inj_gt_iff. Qed.
 
 Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H]; intro y; destruct y as [| m];
-    [ simpl in |- *; trivial with arith
-      | simpl in |- *; trivial with arith
-      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
-      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
-	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
-	  trivial with arith ].
+ induction n as [|n IH]; intros [|m]; simpl; trivial.
+ rewrite <- plus_n_O; trivial.
+ change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)).
+ now rewrite inj_S, IH, 2 inj_S, Zplus_succ_l.
 Qed.
 
 Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H];
-    [ simpl in |- *; trivial with arith
-      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
-	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm;
-	  trivial with arith ].
+ induction n as [|n IH]; intros m; trivial.
+ rewrite inj_S, Zmult_succ_l, <- IH, <- inj_plus.
+ simpl. now rewrite plus_comm.
 Qed.
 
 Theorem inj_minus1 :
   forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m.
 Proof.
-  intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *;
-    rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus;
-      rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r;
-        trivial with arith.
+ intros n m H.
+ apply (Zplus_reg_l (Z_of_nat m)); unfold Zminus.
+ rewrite Zplus_permute, Zplus_opp_r, <- inj_plus, Zplus_0_r.
+ f_equal. symmetry. now apply le_plus_minus.
 Qed.
 
 Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
 Proof.
-  intros x y H; rewrite not_le_minus_0;
-    [ trivial with arith | apply gt_not_le; assumption ].
+ intros. rewrite not_le_minus_0; auto with arith.
 Qed.
 
 Theorem inj_minus : forall n m:nat,
  Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
 Proof.
- intros.
- unfold Zmax.
+ intros n m. unfold Zmax.
  destruct (le_lt_dec m n) as [H|H].
-
+ (* m <= n *)
  rewrite inj_minus1; trivial.
  apply inj_le, Zle_minus_le_0 in H. revert H. unfold Zle.
  case Zcompare_spec; intuition.
-
+ (* n < m *)
  rewrite inj_minus2; trivial.
  apply inj_lt, Zlt_gt in H.
  apply (Zplus_gt_compat_r _ _ (- Z_of_nat m)) in H.
@@ -192,59 +174,170 @@ Theorem inj_min : forall n m:nat,
   Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
 Proof.
  intros n m. unfold Zmin. rewrite inj_compare.
- case nat_compare_spec; intros; f_equal.
- subst. apply min_idempotent.
- apply min_l. auto with arith.
- apply min_r. auto with arith.
+ case nat_compare_spec; intros; f_equal; subst; auto with arith.
 Qed.
 
 Theorem inj_max : forall n m:nat,
   Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
 Proof.
  intros n m. unfold Zmax. rewrite inj_compare.
- case nat_compare_spec; intros; f_equal.
- subst. apply max_idempotent.
- apply max_r. auto with arith.
- apply max_l. auto with arith.
+ case nat_compare_spec; intros; f_equal; subst; auto with arith.
 Qed.
 
 (** Composition of injections **)
 
-Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
-  forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
+Lemma Z_of_nat_of_P : forall p, Z_of_nat (nat_of_P p) = Zpos p.
 Proof.
-  intros x; elim x; simpl in |- *; auto.
-  intros p H; rewrite ZL6.
-  apply f_equal with (f := Zpos).
-  apply nat_of_P_inj.
-  rewrite nat_of_P_o_P_of_succ_nat_eq_succ; unfold nat_of_P in |- *;
-    simpl in |- *.
-  rewrite ZL6; auto.
-  intros p H; unfold nat_of_P in |- *; simpl in |- *.
-  rewrite ZL6; simpl in |- *.
-  rewrite inj_plus; repeat rewrite <- H.
-  rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
+ intros p. destruct (nat_of_P_is_S p) as (n,H). rewrite H.
+ simpl. f_equal. rewrite <- (nat_of_P_of_succ_nat n) in H.
+ symmetry. now apply nat_of_P_inj.
 Qed.
 
-(** Misc *)
+(** For compatibility *)
+Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym (Z_of_nat_of_P p).
 
-Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+(******************************************************************)
+(** Properties of the injection from N into Z *)
+
+Lemma Z_of_nat_of_N : forall n, Z_of_nat (nat_of_N n) = Z_of_N n.
 Proof.
-  intros x; exists (Z_of_nat x); split;
-    [ trivial with arith
-      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
-	unfold Zle in |- *; elim x; intros; simpl in |- *;
-          discriminate ].
+  intros [|n]. trivial.
+  simpl. apply Z_of_nat_of_P.
 Qed.
 
-Lemma Zpos_P_of_succ_nat : forall n:nat,
- Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Lemma Z_of_N_of_nat : forall n, Z_of_N (N_of_nat n) = Z_of_nat n.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
+Proof.
+ intros; f_equal; assumption.
+Qed.
+
+Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
+Proof.
+ intros [|n] [|m]; simpl; congruence.
+Qed.
+
+Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
+Proof.
+ split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
+Qed.
+
+Lemma Z_of_N_compare : forall n m,
+ Zcompare (Z_of_N n) (Z_of_N m) = Ncompare n m.
+Proof.
+ intros [|n] [|m]; trivial.
+Qed.
+
+Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> Z_of_N n <= Z_of_N m.
+Proof.
+ intros. unfold Zle. now rewrite Z_of_N_compare.
+Qed.
+
+Lemma Z_of_N_le : forall n m, (n<=m)%N -> Z_of_N n <= Z_of_N m.
+Proof.
+ apply Z_of_N_le_iff.
+Qed.
+
+Lemma Z_of_N_le_rev : forall n m, Z_of_N n <= Z_of_N m -> (n<=m)%N.
+Proof.
+ apply Z_of_N_le_iff.
+Qed.
+
+Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> Z_of_N n < Z_of_N m.
+Proof.
+ intros. unfold Zlt. now rewrite Z_of_N_compare.
+Qed.
+
+Lemma Z_of_N_lt : forall n m, (n<m)%N -> Z_of_N n < Z_of_N m.
+Proof.
+ apply Z_of_N_lt_iff.
+Qed.
+
+Lemma Z_of_N_lt_rev : forall n m, Z_of_N n < Z_of_N m -> (n<m)%N.
+Proof.
+ apply Z_of_N_lt_iff.
+Qed.
+
+Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> Z_of_N n >= Z_of_N m.
+Proof.
+ intros. unfold Zge. now rewrite Z_of_N_compare.
+Qed.
+
+Lemma Z_of_N_ge : forall n m, (n>=m)%N -> Z_of_N n >= Z_of_N m.
+Proof.
+ apply Z_of_N_ge_iff.
+Qed.
+
+Lemma Z_of_N_ge_rev : forall n m, Z_of_N n >= Z_of_N m -> (n>=m)%N.
+Proof.
+ apply Z_of_N_ge_iff.
+Qed.
+
+Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> Z_of_N n > Z_of_N m.
+Proof.
+ intros. unfold Zgt. now rewrite Z_of_N_compare.
+Qed.
+
+Lemma Z_of_N_gt : forall n m, (n>m)%N -> Z_of_N n > Z_of_N m.
+Proof.
+ apply Z_of_N_gt_iff.
+Qed.
+
+Lemma Z_of_N_gt_rev : forall n m, Z_of_N n > Z_of_N m -> (n>m)%N.
+Proof.
+ apply Z_of_N_gt_iff.
+Qed.
+
+Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+Proof.
+ now destruct z.
+Qed.
+
+Lemma Z_of_N_le_0 : forall n, 0 <= Z_of_N n.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Z_of_N_plus : forall n m, Z_of_N (n+m) = Z_of_N n + Z_of_N m.
+Proof.
+ now destruct n, m.
+Qed.
+
+Lemma Z_of_N_mult : forall n m, Z_of_N (n*m) = Z_of_N n * Z_of_N m.
+Proof.
+ now destruct n, m.
+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.
+ case Pcompare_spec; intros H.
+ subst. now rewrite Pminus_mask_diag.
+ rewrite Pminus_mask_Lt; trivial.
+ unfold Pminus.
+ destruct (Pminus_mask_Gt n m (ZC2 _ _ H)) as (q & -> & _); trivial.
+Qed.
+
+Lemma Z_of_N_succ : forall n, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).
+Proof.
+ intros [|n]; simpl; trivial. now rewrite Zpos_succ_morphism.
+Qed.
+
+Lemma Z_of_N_min : forall n m, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).
+Proof.
+ intros. unfold Zmin, Nmin. rewrite Z_of_N_compare. now case Ncompare.
+Qed.
+
+Lemma Z_of_N_max : forall n m, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).
 Proof.
-  intros.
-  unfold Z_of_nat.
-  destruct n.
-  simpl; auto.
-  simpl (P_of_succ_nat (S n)).
-  apply Zpos_succ_morphism.
+ intros. unfold Zmax, Nmax. rewrite Z_of_N_compare.
+ case Ncompare_spec; intros; subst; trivial.
 Qed.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 96d05760b..7121393bc 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinInt Zmisc Ring_theory.
+Require Import BinInt BinNat Ring_theory.
 
 Local Open Scope Z_scope.
 
@@ -49,23 +49,38 @@ Proof.
  induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial.
 Qed.
 
-(** An alternative Zpower *)
+Lemma Zpower_Ppow : forall p q, (Zpos p)^(Zpos q) = Zpos (p^q).
+Proof.
+ intros. unfold Ppow, Zpower, Zpower_pos.
+ symmetry. now apply iter_pos_swap_gen.
+Qed.
+
+Lemma Zpower_Npow : forall n m,
+ (Z_of_N n)^(Z_of_N m) = Z_of_N (n^m).
+Proof.
+ intros [|n] [|m]; simpl; trivial.
+ unfold Zpower_pos. generalize 1. induction m; simpl; trivial.
+ apply Zpower_Ppow.
+Qed.
 
-(** This Zpower_opt is extensionnaly equal to Zpower in ZArith,
-    but not convertible with it, and quicker : the number of
-    multiplications is logarithmic instead of linear.
+(** An alternative Zpower *)
 
-    TODO: We should try someday to replace Zpower with this Zpower_opt.
+(** This Zpower_alt is extensionnaly equal to Zpower in ZArith,
+    but not convertible with it. The number of
+    multiplications is logarithmic instead of linear, but
+    these multiplications are bigger. Experimentally, it seems
+    that Zpower_alt is slightly quicker than Zpower on average,
+    but can be quite slower on powers of 2.
 *)
 
-Definition Zpower_opt n m :=
+Definition Zpower_alt n m :=
   match m with
     | Z0 => 1
     | Zpos p => Piter_op Zmult p n
     | Zneg p => 0
   end.
 
-Infix "^^" := Zpower_opt (at level 30, right associativity) : Z_scope.
+Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
 
 Lemma iter_pos_mult_acc : forall f,
  (forall x y:Z, (f x)*y = f (x*y)) ->
@@ -92,7 +107,7 @@ Qed.
 Lemma Zpower_equiv : forall a b, a^^b = a^b.
 Proof.
  intros a [|p|p]; trivial.
- unfold Zpower_opt, Zpower, Zpower_pos.
+ unfold Zpower_alt, Zpower, Zpower_pos.
  revert a.
  induction p; simpl; intros.
  f_equal.
@@ -105,17 +120,22 @@ Proof.
  now rewrite Zmult_1_r.
 Qed.
 
-Lemma Zpower_opt_0_r : forall n, n^^0 = 1.
+Lemma Zpower_alt_0_r : forall n, n^^0 = 1.
 Proof. reflexivity. Qed.
 
-Lemma Zpower_opt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b.
+Lemma Zpower_alt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b.
 Proof.
  intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
  now rewrite Zmult_1_r.
  rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
 Qed.
 
-Lemma Zpower_opt_neg_r : forall a b, b<0 -> a^^b = 0.
+Lemma Zpower_alt_neg_r : forall a b, b<0 -> a^^b = 0.
 Proof.
  now destruct b.
 Qed.
+
+Lemma Zpower_alt_Ppow : forall p q, (Zpos p)^^(Zpos q) = Zpos (p^q).
+Proof.
+ intros. now rewrite Zpower_equiv, Zpower_Ppow.
+Qed.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index e08b7ebc3..c021b01a9 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -55,7 +55,7 @@ Proof.
   rewrite (Zpower_pos_nat z n).
   rewrite (Zpower_pos_nat z m).
   rewrite (Zpower_pos_nat z (n + m)).
-  rewrite (nat_of_P_plus_morphism n m).
+  rewrite (Pplus_plus n m).
   apply Zpower_nat_is_exp.
 Qed.