Cleanup of files related with power over Z.

 - Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z

 - The alternative Zpower_alt is now in a separate file Zpow_alt.v,
   not loaded by default.

 - Some more injection lemmas in Znat (pow, div, mod, quot, rem)

 - Btw, added a "square" function in Z, N, Pos, ... (instead of
   Zpow_facts.Zsquare).

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

19 files changed, 635 insertions, 656 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 228be4d1a..418fd8e58 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -442,6 +442,13 @@ Proof.
  now destruct p.
 Qed.
 
+(** Specification of square *)
+
+Lemma square_spec n : square n = n * n.
+Proof.
+ destruct n; trivial. simpl. f_equal. apply Pos.square_spec.
+Qed.
+
 (** Specification of Base-2 logarithm *)
 
 Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index d459f8509..d7660422a 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -181,6 +181,14 @@ Definition pow n p :=
 
 Infix "^" := pow : N_scope.
 
+(** Square *)
+
+Definition square n :=
+  match n with
+    | 0 => 0
+    | Npos p => Npos (Pos.square p)
+  end.
+
 (** Base-2 logarithm *)
 
 Definition log2 n :=
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index a5be98aab..fd20ce725 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -114,9 +114,9 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
 Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
    <+ HasAbs <+ HasSgn <+ NZParity.NZParity
    <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
-   <+ ZDiv <+ ZQuot <+ NZBits.NZBits.
+   <+ ZDiv <+ ZQuot <+ NZBits.NZBits <+ NZSquare.
 
 Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
    <+ HasAbs <+ HasSgn <+ NZParity.NZParity
    <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
-   <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'.
+   <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits' <+ NZSquare.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 5a0f590ba..bfbc063ce 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -14,7 +14,7 @@ Module ZTypeIsZAxioms (Import ZZ : ZType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
- spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
+ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt
  spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
  spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
  spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
@@ -303,6 +303,13 @@ Proof.
  intros a b. red. now rewrite spec_pow_N, spec_pow_pos.
 Qed.
 
+(** Square *)
+
+Lemma square_spec n : square n == n * n.
+Proof.
+ now zify.
+Qed.
+
 (** Sqrt *)
 
 Lemma sqrt_spec : forall n, 0<=n ->
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 4dedcfe32..fcd98787f 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -137,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
 Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
 Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
 
+(** A square function *)
+
+Module Type NZSquare (Import NZ : NZBasicFunsSig').
+ Parameter Inline square : t -> t.
+ Axiom square_spec : forall n, square n == n * n.
+End NZSquare.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 45a2cf3e1..ca6ccc1bf 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -34,11 +34,11 @@ End NDivSpecific.
 
 Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
   <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
-  <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
+  <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits <+ NZSquare.
 
 Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
   <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
-  <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
+  <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits' <+ NZSquare.
 
 
 (** It could also be interesting to have a constructive recursor function. *)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index b6b26363e..d5df6329a 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -53,6 +53,11 @@ Proof. reflexivity. Qed.
 Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b.
 Proof. reflexivity. Qed.
 
+Definition square n := n * n.
+
+Lemma square_spec n : square n = n * n.
+Proof. reflexivity. Qed.
+
 Definition Even n := exists m, n = 2*m.
 Definition Odd n := exists m, n = 2*m+1.
 
@@ -737,6 +742,9 @@ Definition pow_succ_r := pow_succ_r.
 Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
 Definition pow := pow.
 
+Definition square := square.
+Definition square_spec := square_spec.
+
 Definition log2_spec := log2_spec.
 Definition log2_nonpos := log2_nonpos.
 Definition log2 := log2.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index cfe842b9d..aaf44ca64 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -83,7 +83,7 @@ Module Type NType.
  Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
  Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
- Parameter spec_square: forall x, [square x] = [x] *  [x].
+ Parameter spec_square: forall x, [square x] = [x] * [x].
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index adbd8223a..a0ad7643d 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import NN : NType').
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
- spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
- spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
+ spec_square spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N
+ spec_pow spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
  spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
  : nsimpl.
 Ltac nsimpl := autorewrite with nsimpl.
@@ -256,6 +256,13 @@ Proof.
  intros. now zify.
 Qed.
 
+(** Square *)
+
+Lemma square_spec n : square n == n * n.
+Proof.
+ now zify.
+Qed.
+
 (** Sqrt *)
 
 Lemma sqrt_spec : forall n, 0<=n ->
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 956421785..2e4d52a29 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -629,6 +629,16 @@ Proof.
  unfold pow. now rewrite iter_succ.
 Qed.
 
+(** ** Properties of square *)
+
+Lemma square_spec p : square p = p * p.
+Proof.
+ induction p.
+ - rewrite square_xI. simpl. now rewrite IHp.
+ - rewrite square_xO. simpl. now rewrite IHp.
+ - trivial.
+Qed.
+
 (** ** Properties of [sub_mask] *)
 
 Lemma sub_mask_succ_r p q :
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index b6b7ab7a5..7916511a4 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -210,6 +210,15 @@ Definition pow (x y:positive) := iter y (mul x) 1.
 
 Infix "^" := pow : positive_scope.
 
+(** ** Square *)
+
+Fixpoint square p :=
+  match p with
+    | p~1 => (square p + p)~0~1
+    | p~0 => (square p)~0~0
+    | 1 => 1
+  end.
+
 (** ** Division by 2 rounded below but for 1 *)
 
 Definition div2 p :=
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 9e559b68c..4f6fb39c5 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -576,6 +576,20 @@ Proof.
  now destruct m.
 Qed.
 
+(** For folding back a [pow_pos] into a [pow] *)
+
+Lemma pow_pos_fold n p : pow_pos n p = n ^ (Zpos p).
+Proof.
+ reflexivity.
+Qed.
+
+(** ** Specification of square *)
+
+Lemma square_spec n : square n = n * n.
+Proof.
+ destruct n; trivial; simpl; f_equal; apply Pos.square_spec.
+Qed.
+
 (** ** Specification of square root *)
 
 Lemma sqrtrem_spec n : 0<=n ->
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index ee9051ff8..d96d20fbb 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -132,6 +132,15 @@ Definition pow x y :=
 
 Infix "^" := pow : Z_scope.
 
+(** ** Square *)
+
+Definition square x :=
+  match x with
+    | 0 => 0
+    | Zpos p => Zpos (Pos.square p)
+    | Zneg p => Zpos (Pos.square p)
+  end.
+
 (** ** Comparison *)
 
 Definition compare x y :=
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 0ae5dea81..e3843990c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -212,6 +212,36 @@ Proof.
  case N.compare_spec; intros; subst; trivial.
 Qed.
 
+Lemma inj_div n m : Z.of_N (n/m) = Z.of_N n / Z.of_N m.
+Proof.
+ destruct m as [|m]. now destruct n.
+ apply Z.div_unique_pos with (Z.of_N (n mod (Npos m))).
+ split. apply is_nonneg. apply inj_lt. now apply N.mod_lt.
+ rewrite <- inj_mul, <- inj_add. f_equal. now apply N.div_mod.
+Qed.
+
+Lemma inj_mod n m : (m<>0)%N -> Z.of_N (n mod m) = (Z.of_N n) mod (Z.of_N m).
+Proof.
+ intros Hm.
+ apply Z.mod_unique_pos with (Z.of_N (n / m)).
+ split. apply is_nonneg. apply inj_lt. now apply N.mod_lt.
+ rewrite <- inj_mul, <- inj_add. f_equal. now apply N.div_mod.
+Qed.
+
+Lemma inj_quot n m : Z.of_N (n/m) = Z.of_N n ÷ Z.of_N m.
+Proof.
+ destruct m.
+ - now destruct n.
+ - rewrite Z.quot_div_nonneg, inj_div; trivial. apply is_nonneg. easy.
+Qed.
+
+Lemma inj_rem n m : Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m).
+Proof.
+ destruct m.
+ - now destruct n.
+ - rewrite Z.rem_mod_nonneg, inj_mod; trivial. easy. apply is_nonneg. easy.
+Qed.
+
 Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n).
 Proof.
  destruct n as [|p]; trivial. now destruct p.
@@ -222,6 +252,11 @@ Proof.
  destruct n as [|p]; trivial. now destruct p.
 Qed.
 
+Lemma inj_pow n m : Z.of_N (n^m) = (Z.of_N n)^(Z.of_N m).
+Proof.
+ symmetry. destruct n, m; trivial. now apply Z.pow_0_l. apply Z.pow_Zpos.
+Qed.
+
 End N2Z.
 
 Module Z2N.
@@ -323,6 +358,56 @@ Proof.
   now case Pos.compare.
 Qed.
 
+Lemma inj_div n m : 0<=n -> 0<=m -> Z.to_N (n/m) = (Z.to_N n / Z.to_N m)%N.
+Proof.
+ destruct n, m; trivial; intros Hn Hm;
+ (now destruct Hn) || (now destruct Hm) || clear.
+ simpl. rewrite <- (N2Z.id (_ / _)). f_equal. now rewrite N2Z.inj_div.
+Qed.
+
+Lemma inj_mod n m : 0<=n -> 0<m ->
+ Z.to_N (n mod m) = ((Z.to_N n) mod (Z.to_N m))%N.
+Proof.
+ destruct n, m; trivial; intros Hn Hm;
+ (now destruct Hn) || (now destruct Hm) || clear.
+ simpl. rewrite <- (N2Z.id (_ mod _)). f_equal. now rewrite N2Z.inj_mod.
+Qed.
+
+Lemma inj_quot n m : 0<=n -> 0<=m -> Z.to_N (n÷m) = (Z.to_N n / Z.to_N m)%N.
+Proof.
+ destruct m.
+ - now destruct n.
+ - intros. now rewrite Z.quot_div_nonneg, inj_div.
+ - now destruct 2.
+Qed.
+
+Lemma inj_rem n m :0<=n -> 0<=m ->
+ Z.to_N (Z.rem n m) = ((Z.to_N n) mod (Z.to_N m))%N.
+Proof.
+ destruct m.
+ - now destruct n.
+ - intros. now rewrite Z.rem_mod_nonneg, inj_mod.
+ - now destruct 2.
+Qed.
+
+Lemma inj_div2 n : Z.to_N (Z.div2 n) = N.div2 (Z.to_N n).
+Proof.
+ destruct n as [|p|p]; trivial. now destruct p.
+Qed.
+
+Lemma inj_quot2 n : Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n).
+Proof.
+ destruct n as [|p|p]; trivial; now destruct p.
+Qed.
+
+Lemma inj_pow n m : 0<=n -> 0<=m -> Z.to_N (n^m) = ((Z.to_N n)^(Z.to_N m))%N.
+Proof.
+ destruct m.
+ - trivial.
+ - intros. now rewrite <- (N2Z.id (_ ^ _)), N2Z.inj_pow, id.
+ - now destruct 2.
+Qed.
+
 End Z2N.
 
 Module Zabs2N.
@@ -369,6 +454,11 @@ Qed.
 
 (** [Z.abs_N] and usual operations, with non-negative integers *)
 
+Lemma inj_opp n : Z.abs_N (-n) = Z.abs_N n.
+Proof.
+ now destruct n.
+Qed.
+
 Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).
 Proof.
  intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_succ.
@@ -430,6 +520,35 @@ Proof.
  transitivity n; trivial. apply Z.le_max_l.
 Qed.
 
+Lemma inj_quot n m : Z.abs_N (n÷m) = ((Z.abs_N n) / (Z.abs_N m))%N.
+Proof.
+ assert (forall p q, Z.abs_N (Zpos p ÷ Zpos q) = (Npos p / Npos q)%N).
+  intros. rewrite abs_N_nonneg. now apply Z2N.inj_quot. now apply Z.quot_pos.
+ destruct n, m; trivial; simpl.
+ - trivial.
+ - now rewrite <- Z.opp_Zpos, Z.quot_opp_r, inj_opp.
+ - now rewrite <- Z.opp_Zpos, Z.quot_opp_l, inj_opp.
+ - now rewrite <- 2 Z.opp_Zpos, Z.quot_opp_opp.
+Qed.
+
+Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N.
+Proof.
+ assert
+  (forall p q, Z.abs_N (Z.rem (Zpos p) (Zpos q)) = ((Npos p) mod (Npos q))%N).
+  intros. rewrite abs_N_nonneg. now apply Z2N.inj_rem. now apply Z.rem_nonneg.
+ destruct n, m; trivial; simpl.
+ - trivial.
+ - now rewrite <- Z.opp_Zpos, Z.rem_opp_r.
+ - now rewrite <- Z.opp_Zpos, Z.rem_opp_l, inj_opp.
+ - now rewrite <- 2 Z.opp_Zpos, Z.rem_opp_opp, inj_opp.
+Qed.
+
+Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N.
+Proof.
+ intros Hm. rewrite abs_N_spec, Z.abs_pow, Z2N.inj_pow, <- abs_N_spec; trivial.
+ f_equal. symmetry; now apply abs_N_nonneg. apply Z.abs_nonneg.
+Qed.
+
 (** [Z.abs_N] and usual operations, statements with [Z.abs] *)
 
 Lemma inj_succ_abs n : Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n).
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
new file mode 100644
index 000000000..a90eedb41
--- /dev/null
+++ b/theories/ZArith/Zpow_alt.v
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import BinInt.
+Local Open Scope Z_scope.
+
+(** An alternative power function for Z *)
+
+(** This [Zpower_alt] is extensionnaly equal to [Z.pow],
+    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 [Z.pow] on average,
+    but can be quite slower on powers of 2.
+*)
+
+Definition Zpower_alt n m :=
+  match m with
+    | Z0 => 1
+    | Zpos p => Pos.iter_op Z.mul p n
+    | Zneg p => 0
+  end.
+
+Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
+
+Lemma Piter_mul_acc : forall f,
+ (forall x y:Z, (f x)*y = f (x*y)) ->
+ forall p k, Pos.iter p f k = (Pos.iter p f 1)*k.
+Proof.
+ intros f Hf.
+ induction p; simpl; intros.
+ - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc.
+ - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc.
+ - now rewrite Hf, Z.mul_1_l.
+Qed.
+
+Lemma Piter_op_square : forall p a,
+ Pos.iter_op Z.mul p (a*a) = (Pos.iter_op Z.mul p a)*(Pos.iter_op Z.mul p a).
+Proof.
+ induction p; simpl; intros; trivial. now rewrite IHp, Z.mul_shuffle1.
+Qed.
+
+Lemma Zpower_equiv a b : a^^b = a^b.
+Proof.
+ destruct b as [|p|p]; trivial.
+ unfold Zpower_alt, Z.pow, Z.pow_pos.
+ revert a.
+ induction p; simpl; intros.
+ - f_equal.
+   rewrite Piter_mul_acc.
+   now rewrite Piter_op_square, IHp.
+   intros. symmetry; apply Z.mul_assoc.
+ - rewrite Piter_mul_acc.
+   now rewrite Piter_op_square, IHp.
+   intros. symmetry; apply Z.mul_assoc.
+ - now Z.nzsimpl.
+Qed.
+
+Lemma Zpower_alt_0_r n : n^^0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpower_alt_succ_r a b : 0<=b -> a^^(Z.succ b) = a * a^^b.
+Proof.
+ destruct b as [|b|b]; intros Hb; simpl.
+ - now Z.nzsimpl.
+ - now rewrite Pos.add_1_r, Pos.iter_op_succ by apply Z.mul_assoc.
+ - now elim Hb.
+Qed.
+
+Lemma Zpower_alt_neg_r a b : b<0 -> a^^b = 0.
+Proof.
+ now destruct b.
+Qed.
+
+Lemma Zpower_alt_Ppow p q : (Zpos p)^^(Zpos q) = Zpos (p^q).
+Proof.
+ now rewrite Zpower_equiv, Z.pow_Zpos.
+Qed.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 8307f7601..6f1ebc061 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -6,115 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinInt BinNat Ring_theory.
-
+Require Import BinInt Ring_theory.
 Local Open Scope Z_scope.
 
-(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
-      integer (type [positive]) and [z] a signed integer (type [Z]) *)
+(** * Power functions over [Z] *)
+
+(** Nota : this file is mostly deprecated. The definition of [Z.pow]
+    and its usual properties are now provided by module [BinInt.Z]. *)
 
 Notation Zpower_pos := Z.pow_pos (only parsing).
 Notation Zpower := Z.pow (only parsing).
 Notation Zpower_0_r := Z.pow_0_r (only parsing).
 Notation Zpower_succ_r := Z.pow_succ_r (only parsing).
 Notation Zpower_neg_r := Z.pow_neg_r (only parsing).
+Notation Zpower_Ppow := Z.pow_Zpos (only parsing).
 
-Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.
 Proof.
  constructor. intros.
  destruct n;simpl;trivial.
- unfold Zpower_pos.
- rewrite <- (Zmult_1_r (pow_pos _ _ _)). generalize 1.
- induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial.
-Qed.
-
-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.
-
-(** An alternative Zpower *)
-
-(** 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_alt n m :=
-  match m with
-    | Z0 => 1
-    | Zpos p => Piter_op Zmult p n
-    | Zneg p => 0
-  end.
-
-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)) ->
- forall p k, iter_pos p _ f k = (iter_pos p _ f 1)*k.
-Proof.
- intros f Hf.
- induction p; simpl; intros.
- rewrite IHp. rewrite Hf. f_equal. rewrite (IHp (iter_pos _ _ _ _)).
- rewrite <- Zmult_assoc. f_equal. auto.
- rewrite IHp. rewrite (IHp (iter_pos _ _ _ _)).
- rewrite <- Zmult_assoc. f_equal. auto.
- rewrite Hf. f_equal. now rewrite Zmult_1_l.
-Qed.
-
-Lemma Piter_op_square : forall p a,
- Piter_op Zmult p (a*a) = (Piter_op Zmult p a)*(Piter_op Zmult p a).
-Proof.
- induction p; simpl; intros; trivial.
- rewrite IHp. rewrite <- !Zmult_assoc. f_equal.
- rewrite Zmult_comm, <- Zmult_assoc.
- f_equal. apply Zmult_comm.
-Qed.
-
-Lemma Zpower_equiv : forall a b, a^^b = a^b.
-Proof.
- intros a [|p|p]; trivial.
- unfold Zpower_alt, Zpower, Zpower_pos.
- revert a.
- induction p; simpl; intros.
- f_equal.
- rewrite iter_pos_mult_acc.
- now rewrite Piter_op_square, IHp.
- intros. symmetry; apply Zmult_assoc.
- rewrite iter_pos_mult_acc.
- now rewrite Piter_op_square, IHp.
- intros. symmetry; apply Zmult_assoc.
- now rewrite Zmult_1_r.
-Qed.
-
-Lemma Zpower_alt_0_r : forall n, n^^0 = 1.
-Proof. reflexivity. Qed.
-
-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_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.
+ unfold Z.pow_pos.
+ rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1.
+ induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial.
 Qed.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index d9c5f995b..27e3def4e 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -6,288 +6,104 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith_base.
-Require Import ZArithRing.
-Require Import Zcomplements.
+Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
 Require Export Zpower.
-Require Import Zdiv.
-Require Import Znumtheory.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
-Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
-Proof.
-  intros x; unfold Zpower_pos; simpl; auto with zarith.
-Qed.
-
-Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
-Proof.
-  induction p.
-  (* xI *)
-  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite Zpower_pos_1_r, IHp; auto.
-  (* xO *)
-  rewrite <- Pplus_diag.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite IHp; auto.
-  (* xH *)
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
-Proof.
-  induction p.
-  change (xI p) with (1 + (xO p))%positive.
-  rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
-  rewrite <- Pplus_diag.
-  rewrite Zpower_pos_is_exp, IHp; auto.
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Lemma Zpower_pos_pos: forall x p,
-  0 < x -> 0 < Zpower_pos x p.
-Proof.
-  induction p; intros.
-  (* xI *)
-  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite Zpower_pos_1_r.
-  repeat apply Zmult_lt_0_compat; auto.
-  (* xO *)
-  rewrite <- Pplus_diag.
-  repeat rewrite Zpower_pos_is_exp.
-  repeat apply Zmult_lt_0_compat; auto.
-  (* xH *)
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-
-Theorem Zpower_1_r: forall z, z^1 = z.
-Proof.
-  exact Zpower_pos_1_r.
-Qed.
-
-Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1.
-Proof.
-  destruct z; simpl; auto.
-  intros; apply Zpower_pos_1_l.
-  intros; compute in H; elim H; auto.
-Qed.
-
-Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0.
-Proof.
-  destruct z; simpl; auto with zarith.
-  intros; apply Zpower_pos_0_l.
-Qed.
+(** Properties of the power function over [Z] *)
 
-Theorem Zpower_0_r: forall z, z^0 = 1.
-Proof.
-  simpl; auto.
-Qed.
+(** Nota: the usual properties of [Z.pow] are now already provided
+    by [BinInt.Z]. Only remain here some compatibility elements,
+    as well as more specific results about power and modulo and/or
+    primality. *)
 
-Theorem Zpower_2: forall z, z^2 = z * z.
-Proof.
-  intros; ring.
-Qed.
+Lemma Zpower_pos_1_r x : Z.pow_pos x 1 = x.
+Proof (Z.pow_1_r x).
 
-Theorem Zpower_gt_0: forall x y,
-  0 < x -> 0 <= y -> 0 < x^y.
-Proof.
-  destruct y; simpl; auto with zarith.
-  intros; apply Zpower_pos_pos; auto.
-  intros; compute in H0; elim H0; auto.
-Qed.
+Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1.
+Proof. now apply (Z.pow_1_l (Zpos p)). Qed.
 
-Theorem Zpower_Zabs: forall a b,  Zabs (a^b) = (Zabs a)^b.
-Proof.
-  intros a b; case (Zle_or_lt 0 b).
-  intros Hb; pattern b; apply natlike_ind; auto with zarith.
-  intros x Hx Hx1; unfold Zsucc.
-  (repeat rewrite Zpower_exp); auto with zarith.
-  rewrite Zabs_Zmult; rewrite Hx1.
-  f_equal; auto.
-  replace (a ^ 1) with a; auto.
-  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
-  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
-  case b; simpl; auto with zarith.
-  intros p Hp; discriminate.
-Qed.
+Lemma Zpower_pos_0_l p : Z.pow_pos 0 p = 0.
+Proof. now apply (Z.pow_0_l (Zpos p)). Qed.
 
-Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n.
-Proof.
-  intros p n H.
-  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
-  rewrite Zpower_1_r; apply Zmult_comm.
-Qed.
+Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.
+Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed.
 
-Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r.
-Proof.
-  intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto.
-  intros H3; rewrite Zmult_0_r; repeat rewrite Zpower_exp_0; auto.
-  intros r1 H3 H4 H5.
-  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
-  rewrite <- H4; try rewrite Zpower_1_r; try rewrite <- Zpower_exp; try f_equal; auto with zarith.
-  ring.
-  apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto.
-Qed.
+Notation Zpower_1_r := Z.pow_1_r (only parsing).
+Notation Zpower_1_l := Z.pow_1_l (only parsing).
+Notation Zpower_0_l := Z.pow_0_l' (only parsing).
+Notation Zpower_0_r := Z.pow_0_r (only parsing).
+Notation Zpower_2 := Z.pow_2_r (only parsing).
+Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing).
+Notation Zpower_ge_0 := Z.pow_nonneg (only parsing).
+Notation Zpower_Zabs := Z.abs_pow (only parsing).
+Notation Zpower_Zsucc := Z.pow_succ_r (only parsing).
+Notation Zpower_mult := Z.pow_mul_r (only parsing).
+Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing).
 
-Theorem Zpower_le_monotone: forall a b c,
+Theorem Zpower_le_monotone a b c :
  0 < a -> 0 <= b <= c -> a^b <= a^c.
-Proof.
-  intros a b c H (H1, H2).
-  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
-  rewrite Zpower_exp; auto with zarith.
-  apply Zmult_le_compat_l; auto with zarith.
-  assert (0 < a ^ (c - b)); auto with zarith.
-  apply Zpower_gt_0; auto with zarith.
-  apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
-Qed.
+Proof. intros. now apply Z.pow_le_mono_r. Qed.
 
-Theorem Zpower_lt_monotone: forall a b c,
+Theorem Zpower_lt_monotone a b c :
  1 < a -> 0 <= b < c -> a^b < a^c.
-Proof.
-  intros a b c H (H1, H2).
-  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
-  rewrite Zpower_exp; auto with zarith.
-  apply Zmult_lt_compat_l; auto with zarith.
-  apply Zpower_gt_0; auto with zarith.
-  assert (0 < a ^ (c - b)); auto with zarith.
-  apply Zpower_gt_0; auto with zarith.
-  apply Zlt_le_trans with (a ^1); auto with zarith.
-  rewrite Zpower_1_r; auto with zarith.
-  apply Zpower_le_monotone; auto with zarith.
-Qed.
-
-Theorem Zpower_gt_1 : forall x y,
-  1 < x -> 0 < y -> 1 < x^y.
-Proof.
-  intros x y H1 H2.
-  replace 1 with (x ^ 0) by apply Zpower_0_r.
-  apply Zpower_lt_monotone; auto with zarith.
-Qed.
+Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed.
 
-Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y.
-Proof.
-  intros x y; case y; auto with zarith.
-  simpl ; auto with zarith.
-  intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
-  generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith.
-  intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.
-  apply Zmult_le_0_compat; auto with zarith.
-  generalize H1; case x; compute; intros; auto; try discriminate.
-Qed.
-
-Theorem Zpower_le_monotone2:
-   forall a b c, 0 < a -> b <= c -> a^b <= a^c.
-Proof.
-  intros a b c H H2.
-  destruct (Z_le_gt_dec 0 b) as [Hb|Hb].
-  apply Zpower_le_monotone; auto.
-  replace (a^b) with 0.
-  destruct (Z_le_gt_dec 0 c) as [Hc|Hc].
-  destruct (Zle_lt_or_eq _ _ Hc) as [Hc'|Hc'].
-  apply Zlt_le_weak;apply Zpower_gt_0;trivial.
-  rewrite <- Hc';simpl;auto with zarith.
-  replace (a^c) with 0. auto with zarith.
-  destruct c;trivial;unfold Zgt in Hc;discriminate Hc.
-  destruct b;trivial;unfold Zgt in Hb;discriminate Hb.
-Qed.
+Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y.
+Proof. apply Z.pow_gt_1. Qed.
 
-Theorem Zmult_power: forall p q r, 0 <= r ->
-  (p*q)^r = p^r * q^r.
-Proof.
-  intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto.
-  clear r H1; intros r H1 H2 H3.
-  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
-  rewrite H2; repeat rewrite Zpower_exp; auto with zarith; ring.
-Qed.
+Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.
+Proof. intros. apply Z.pow_mul_l. Qed.
 
-Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith.
+Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
 
-Theorem Zpower_le_monotone3: forall a b c,
+Theorem Zpower_le_monotone3 a b c :
  0 <= c -> 0 <= a <= b -> a^c <= b^c.
-Proof.
-  intros a b c H (H1, H2).
-  generalize H; pattern c; apply natlike_ind; auto.
-  intros x HH HH1 _; unfold Zsucc; repeat rewrite Zpower_exp; auto with zarith.
-  repeat rewrite Zpower_1_r.
-  apply Zle_trans with (a^x * b); auto with zarith.
-Qed.
+Proof. intros. now apply Z.pow_le_mono_l. Qed.
 
-Lemma Zpower_le_monotone_inv: forall a b c,
+Lemma Zpower_le_monotone_inv a b c :
   1 < a -> 0 < b -> a^b <= a^c -> b <= c.
 Proof.
-  intros a b c H H0 H1.
-  destruct (Z_le_gt_dec b c);trivial.
-  assert (2 <= a^b).
-   apply Zle_trans with (2^b).
-   pattern 2 at 1;replace 2 with (2^1);trivial.
-   apply Zpower_le_monotone;auto with zarith.
-   apply Zpower_le_monotone3;auto with zarith.
-  assert (c > 0).
-  destruct (Z_le_gt_dec 0 c) as [Hc|Hc];trivial.
-  destruct (Zle_lt_or_eq _ _ Hc);auto with zarith.
-  rewrite <- H3 in H1;simpl in H1; exfalso;omega.
-  destruct c;try discriminate Hc. simpl in H1. exfalso;omega.
-  assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega.
+ intros Ha Hb H. apply (Z.pow_le_mono_r_iff a); trivial.
+ apply Z.lt_le_incl; apply (Z.pow_gt_1 a); trivial.
+ apply Z.lt_le_trans with (a^b); trivial. now apply Z.pow_gt_1.
 Qed.
 
-Theorem Zpower_nat_Zpower: forall p q, 0 <= q ->
- p^q = Zpower_nat p (Zabs_nat q).
-Proof.
-  intros p1 q1; case q1; simpl.
-  intros _; exact (refl_equal _).
-  intros p2 _; apply Zpower_pos_nat.
-  intros p2 H1; case H1; auto.
-Qed.
+Notation Zpower_nat_Zpower := Zpower_nat_Zpower (only parsing).
 
-Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n.
-Proof.
-  intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n.
-  simpl; auto with zarith.
-  intros n H1 H2; unfold Zsucc.
-  case (Zle_lt_or_eq _ _ H1); clear H1; intros H1.
-  apply Zle_lt_trans with (n + n); auto with zarith.
-  rewrite Zpower_exp; auto with zarith.
-  rewrite Zpower_1_r.
-  assert (tmp: forall p, p * 2 = p + p); intros; try ring;
-  rewrite tmp; auto with zarith.
-  subst n; simpl; unfold Zpower_pos; simpl; auto with zarith.
-Qed.
+Theorem Zpower2_lt_lin n : 0 <= n -> n < 2^n.
+Proof. intros. now apply Z.pow_gt_lin_r. Qed.
 
-Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n.
-Proof.
-  intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto.
-Qed.
+Theorem Zpower2_le_lin n : 0 <= n -> n <= 2^n.
+Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed.
 
-Lemma Zpower2_Psize :
-  forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat.
+Lemma Zpower2_Psize n p :
+  Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.
 Proof.
-  induction n.
-  destruct p; split; intros H; discriminate H || inversion H.
-  destruct p; simpl Psize.
-  rewrite inj_S, Zpower_Zsucc; auto with zarith.
-  rewrite Zpos_xI; specialize IHn with p; omega.
-  rewrite inj_S, Zpower_Zsucc; auto with zarith.
-  rewrite Zpos_xO; specialize IHn with p; omega.
-  split; auto with arith.
-  intros _; apply Zpower_gt_1; auto with zarith.
-  rewrite inj_S; generalize (Zle_0_nat n); omega.
+  revert p; induction n.
+  destruct p; now split.
+  assert (Hn := Nat2Z.is_nonneg n).
+  destruct p; simpl Pos.size_nat.
+  - specialize IHn with p.
+    rewrite Z.pos_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega.
+  - specialize IHn with p.
+    rewrite Z.pos_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega.
+  - split; auto with zarith.
+    intros _. apply Z.pow_gt_1. easy.
+    now rewrite Nat2Z.inj_succ, Z.lt_succ_r.
 Qed.
 
 (** * Zpower and modulo *)
 
-Theorem Zpower_mod: forall p q n, 0 < n ->
- (p^q) mod n = ((p mod n)^q) mod n.
+Theorem Zpower_mod p q n :
+  0 < n -> (p^q) mod n = ((p mod n)^q) mod n.
 Proof.
-  intros p q n Hn; case (Zle_or_lt 0 q); intros H1.
-  generalize H1; pattern q; apply natlike_ind; auto.
-  intros q1 Hq1 Rec _; unfold Zsucc; repeat rewrite Zpower_exp; repeat rewrite Zpower_1_r; auto with zarith.
-  rewrite (fun x => (Zmult_mod x p)); try rewrite Rec; auto with zarith.
-  rewrite (fun x y => (Zmult_mod (x ^y))); try f_equal; auto with zarith.
-  f_equal; auto; apply sym_equal; apply Zmod_mod; auto with zarith.
-  generalize H1; case q; simpl; auto.
-  intros; discriminate.
+  intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1].
+  - pattern q; apply natlike_ind; trivial.
+    clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial.
+    rewrite Z.mul_mod_idemp_l; auto with zarith.
+    rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith.
+  - rewrite !Z.pow_neg_r; auto with zarith.
 Qed.
 
 (** A direct way to compute Zpower modulo **)
@@ -311,153 +127,113 @@ Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z :=
 
 Definition Zpow_mod a m n :=
   match m with
-   | 0 => 1
+   | 0 => 1 mod n
    | Zpos p => Zpow_mod_pos a p n
    | Zneg p => 0
   end.
 
-Theorem Zpow_mod_pos_correct: forall a m n, 0 < n ->
- Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
+Theorem Zpow_mod_pos_correct a m n :
+ n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n.
 Proof.
-  intros a m; elim m; simpl; auto.
-  intros p Rec n H1; rewrite xI_succ_xO, Pplus_one_succ_r, <-Pplus_diag; auto.
-  repeat rewrite Zpower_pos_is_exp; auto.
-  repeat rewrite Rec; auto.
-  rewrite Zpower_pos_1_r.
-  repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith.
-  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith.
-  case (Zpower_pos a p mod n); auto.
-  intros p Rec n H1; rewrite <- Pplus_diag; auto.
-  repeat rewrite Zpower_pos_is_exp; auto.
-  repeat rewrite Rec; auto.
-  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith.
-  case (Zpower_pos a p mod n); auto.
-  unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
+  intros Hn. induction m.
+  - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag.
+    rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r.
+    rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial.
+    rewrite <- IHm, <- Z.mul_mod by trivial.
+    simpl. now destruct (Zpow_mod_pos a m n).
+  - rewrite <- Pos.add_diag at 2.
+    rewrite Zpower_pos_is_exp.
+    rewrite Z.mul_mod by trivial.
+    rewrite <- IHm.
+    simpl. now destruct (Zpow_mod_pos a m n).
+  - now rewrite Zpower_pos_1_r.
 Qed.
 
-Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
- Zpow_mod a m n = (a ^ m) mod n.
+Theorem Zpow_mod_correct a m n :
+ n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
 Proof.
-  intros a m n; case m; simpl.
-  intros; apply sym_equal; apply Zmod_small; auto with zarith.
-  intros; apply Zpow_mod_pos_correct; auto with zarith.
-  intros p H H1; case H1; auto.
+  intros Hn. destruct m; simpl.
+  - trivial.
+  - apply Zpow_mod_pos_correct; auto with zarith.
+  - rewrite Z.mod_0_l; auto with zarith.
 Qed.
 
 (* Complements about power and number theory. *)
 
-Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
+Lemma Zpower_divide p q : 0 < q -> (p | p ^ q).
 Proof.
-  intros p q H; exists (p ^(q - 1)).
-  pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith.
+  exists (p^(q - 1)).
+  rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith.
 Qed.
 
-Theorem rel_prime_Zpower_r: forall i p q, 0 < i ->
- rel_prime p q -> rel_prime p (q^i).
+Theorem rel_prime_Zpower_r i p q :
+ 0 <= i -> rel_prime p q -> rel_prime p (q^i).
 Proof.
-  intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi.
-  intros H; contradict H; auto with zarith.
-  intros i Hi Rec _; rewrite Zpower_Zsucc; auto.
+  intros Hi Hpq; pattern i; apply natlike_ind; auto with zarith.
+  simpl. apply rel_prime_sym, rel_prime_1.
+  clear i Hi. intros i Hi Rec; rewrite Z.pow_succ_r; auto.
   apply rel_prime_mult; auto.
-  case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto.
-  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
 Qed.
 
-Theorem rel_prime_Zpower: forall i j p q, 0 <= i ->  0 <= j ->
- rel_prime p q -> rel_prime (p^i) (q^j).
+Theorem rel_prime_Zpower i j p q :
+ 0 <= i ->  0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j).
 Proof.
-  intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q.
-  intros _ j p q H H1; rewrite Zpower_0_r; apply rel_prime_1.
-  intros n Hn Rec _ j p q Hj Hpq.
-  rewrite Zpower_Zsucc; auto.
-  case Zle_lt_or_eq with (1 := Hj); intros Hj1; subst.
-  apply rel_prime_sym; apply rel_prime_mult; auto.
-  apply rel_prime_sym; apply rel_prime_Zpower_r; auto with arith.
-  apply rel_prime_sym; apply Rec; auto.
-  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+ intros Hi Hj H. apply rel_prime_Zpower_r; trivial.
+ apply rel_prime_sym. apply rel_prime_Zpower_r; trivial.
+ now apply rel_prime_sym.
 Qed.
 
-Theorem prime_power_prime: forall p q n, 0 <= n ->
- prime p -> prime q -> (p | q^n)  -> p = q.
+Theorem prime_power_prime p q n :
+ 0 <= n -> prime p -> prime q -> (p | q^n) -> p = q.
 Proof.
-  intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
-  rewrite Zpower_0_r; intros.
-  assert (2<=p) by (apply prime_ge_2; auto).
-  assert (p<=1) by (apply Zdivide_le; auto with zarith).
-  omega.
-  intros n1 H H1.
-  unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
-  assert (2<=p) by (apply prime_ge_2; auto).
-  assert (2<=q) by (apply prime_ge_2; auto).
-  intros H3; case prime_mult with (2 := H3); auto.
-  intros; apply prime_div_prime; auto.
+  intros Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
+  - simpl; intros.
+    assert (2<=p) by (apply prime_ge_2; auto).
+    assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).
+    omega.
+  - intros n Hn Rec.
+    rewrite Z.pow_succ_r by trivial. intros.
+    assert (2<=p) by (apply prime_ge_2; auto).
+    assert (2<=q) by (apply prime_ge_2; auto).
+    destruct prime_mult with (2 := H); auto.
+    apply prime_div_prime; auto.
 Qed.
 
-Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
- (x | p^n) -> exists m, x = p^m.
+Theorem Zdivide_power_2 x p n :
+ 0 <= n -> 0 <= x -> prime p -> (x | p^n) -> exists m, x = p^m.
 Proof.
-  intros x p n Hn Hx; revert p n Hn; generalize Hx.
+  intros Hn Hx; revert p n Hn. generalize Hx.
   pattern x; apply Z_lt_induction; auto.
   clear x Hx; intros x IH Hx p n Hn Hp H.
-  case Zle_lt_or_eq with (1 := Hx); auto; clear Hx; intros Hx; subst.
-  case (Zle_lt_or_eq 1 x); auto with zarith; clear Hx; intros Hx; subst.
+  Z.le_elim Hx; subst.
+  apply Z.le_succ_l in Hx; simpl in Hx.
+  Z.le_elim Hx; subst.
   (* x > 1 *)
-  case (prime_dec x); intros H2.
-  exists 1; rewrite Zpower_1_r; apply prime_power_prime with n; auto.
-  case not_prime_divide with (2 := H2); auto.
-  intros p1 ((H3, H4), (q1, Hq1)); subst.
-  case (IH p1) with p n; auto with zarith.
-  apply Zdivide_trans with (2 := H); exists q1; auto with zarith.
-  intros r1 Hr1.
-  case (IH q1) with p n; auto with zarith.
-  case (Zle_lt_or_eq 0 q1).
-  apply Zmult_le_0_reg_r with p1; auto with zarith.
+  case (prime_dec x); intros Hpr.
+  exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto.
+  case not_prime_divide with (2 := Hpr); auto.
+  intros p1 ((Hp1, Hpq1),(q1,->)).
+  assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith).
+  destruct (IH p1) with p n as (r1,Hr1); auto with zarith.
+  transitivity (q1 * p1); trivial. exists q1; auto with zarith.
+  destruct (IH q1) with p n as (r2,Hr2); auto with zarith.
   split; auto with zarith.
-  pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith.
-  apply Zmult_lt_compat_l; auto with zarith.
-  intros H5; subst; contradict Hx; auto with zarith.
-  apply Zmult_le_0_reg_r with p1; auto with zarith.
-  apply Zdivide_trans with (2 := H); exists p1; auto with zarith.
-  intros r2 Hr2; exists (r2 + r1); subst.
-  apply sym_equal; apply Zpower_exp.
-  generalize Hx; case r2; simpl; auto with zarith.
-  intros; red; simpl; intros; discriminate.
-  generalize H3; case r1; simpl; auto with zarith.
-  intros; red; simpl; intros; discriminate.
+  rewrite <- (Z.mul_1_r q1) at 1.
+  apply Z.mul_lt_mono_pos_l; auto with zarith.
+  transitivity (q1 * p1); trivial. exists p1; auto with zarith.
+  exists (r2 + r1); subst.
+  symmetry. apply Z.pow_add_r.
+  generalize Hq1; case r2; now auto with zarith.
+  generalize Hp1; case r1; now auto with zarith.
   (* x = 1 *)
-  exists 0; rewrite Zpower_0_r; auto.
+  exists 0; rewrite Z.pow_0_r; auto.
   (* x = 0 *)
-  exists n; destruct H; rewrite Zmult_0_r in H; auto.
+  exists n; destruct H; rewrite Z.mul_0_r in H; auto.
 Qed.
 
 (** * Zsquare: a direct definition of [z^2] *)
 
-Fixpoint Psquare (p: positive): positive :=
-  match p with
-   | xH => xH
-   | xO p => xO (xO (Psquare p))
-   | xI p => xI (xO (Pplus (Psquare p) p))
-  end.
-
-Definition Zsquare p :=
-  match p with
-   | Z0 => Z0
-   | Zpos p => Zpos (Psquare p)
-   | Zneg p => Zpos (Psquare p)
-  end.
-
-Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.
-Proof.
-  induction p; simpl; auto; f_equal; rewrite IHp.
-  apply trans_equal with (xO p + xO (p*p))%positive; auto.
-  rewrite (Pplus_comm (xO p)); auto.
-  rewrite Pmult_xI_permute_r; rewrite Pplus_assoc.
-  f_equal; auto.
-  symmetry; apply Pplus_diag.
-  symmetry; apply Pmult_xO_permute_r.
-Qed.
-
-Theorem Zsquare_correct: forall p, Zsquare p = p * p.
-Proof.
-  intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto.
-Qed.
+Notation Psquare := Pos.square (only parsing).
+Notation Zsquare := Z.square (only parsing).
+Notation Psquare_correct := Pos.square_spec (only parsing).
+Notation Zsquare_correct := Z.square_spec (only parsing).
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index ce99427f2..5052d01a0 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,70 +6,84 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Wf_nat.
-Require Import ZArith_base.
+Require Import Wf_nat ZArith_base Omega Zcomplements.
 Require Export Zpow_def.
-Require Import Omega.
-Require Import Zcomplements.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
+
+(** * Power functions over [Z] *)
+
+(** Nota : this file is mostly deprecated. The definition of [Z.pow]
+    and its usual properties are now provided by module [BinInt.Z].
+    Powers of 2 are also available there (see [Z.shiftl] and [Z.shiftr]).
+    Only remain here:
+     - [Zpower_nat] : a power function with a [nat] exponent
+     - old-style powers of two, such as [two_p]
+     - [Zdiv_rest] : a division + modulo when the divisor is a power of 2
+*)
 
-(** * Definition of powers over [Z]*)
 
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
+Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.
+
+Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpower_nat_succ_r n z : Zpower_nat z (S n) = z * (Zpower_nat z n).
+Proof. reflexivity. Qed.
 
 (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
-    [plus : nat->nat] and [Zmult : Z->Z] *)
+    [plus : nat->nat->nat] and [Z.mul : Z->Z->Z] *)
 
 Lemma Zpower_nat_is_exp :
   forall (n m:nat) (z:Z),
     Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
 Proof.
-  intros; elim n;
-   [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
-     | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
-       apply Zmult_assoc ].
+ induction n.
+ - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
+ - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc.
+Qed.
+
+(** Conversions between powers of unary and binary integers *)
+
+Lemma Zpower_pos_nat (z : Z) (p : positive) :
+  Z.pow_pos z p = Zpower_nat z (Pos.to_nat p).
+Proof.
+  apply Pos2Nat.inj_iter.
 Qed.
 
-(** This theorem shows that powers of unary and binary integers
-   are the same thing, modulo the function convert : [positive -> nat] *)
+Lemma Zpower_nat_Z (z : Z) (n : nat) :
+  Zpower_nat z n = z ^ (Z.of_nat n).
+Proof.
+ induction n. trivial.
+ rewrite Zpower_nat_succ_r, Nat2Z.inj_succ, Z.pow_succ_r.
+ now f_equal.
+ apply Nat2Z.is_nonneg.
+Qed.
 
-Lemma Zpower_pos_nat :
-  forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
+Theorem Zpower_nat_Zpower z n : 0 <= n ->
+ z^n = Zpower_nat z (Z.abs_nat n).
 Proof.
-  intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
-    apply iter_nat_of_P.
+ intros. now rewrite Zpower_nat_Z, Zabs2Nat.id_abs, Z.abs_eq.
 Qed.
 
-(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
-   deduce that the function [(Zpower_pos z)] is a morphism
-   for [Pplus : positive->positive] and [Zmult : Z->Z] *)
+(** The function [(Z.pow_pos z)] is a morphism
+   for [Pos.add : positive->positive->positive] and [Z.mul : Z->Z->Z] *)
 
-Lemma Zpower_pos_is_exp :
-  forall (n m:positive) (z:Z),
-    Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
+Lemma Zpower_pos_is_exp (n m : positive)(z:Z) :
+  Z.pow_pos z (n + m) = Z.pow_pos z n * Z.pow_pos z m.
 Proof.
-  intros.
-  rewrite (Zpower_pos_nat z n).
-  rewrite (Zpower_pos_nat z m).
-  rewrite (Zpower_pos_nat z (n + m)).
-  rewrite (Pplus_plus n m).
-  apply Zpower_nat_is_exp.
+ now apply (Z.pow_add_r z (Zpos n) (Zpos m)).
 Qed.
 
 Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
 Hint Unfold Zpower_pos Zpower_nat: zarith.
 
-Theorem Zpower_exp :
-  forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+Theorem Zpower_exp x n m :
+  n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
 Proof.
-  destruct n; destruct m; auto with zarith.
-  simpl; intros; apply Zred_factor0.
-  simpl; auto with zarith.
-  intros; compute in H0; elim H0; auto.
-  intros; compute in H; elim H; auto.
+ Z.swap_greater. apply Z.pow_add_r.
 Qed.
 
 Section Powers_of_2.
@@ -80,129 +94,131 @@ Section Powers_of_2.
       calculus is possible. [shift n m] computes [2^n * m], i.e.
       [m] shifted by [n] positions *)
 
-  Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z.
-  Definition shift_pos (n z:positive) := iter_pos n positive xO z.
+  Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z.
+  Definition shift_pos (n z:positive) := Pos.iter n xO z.
   Definition shift (n:Z) (z:positive) :=
     match n with
       | Z0 => z
-      | Zpos p => iter_pos p positive xO z
+      | Zpos p => Pos.iter p xO z
       | Zneg p => z
     end.
 
   Definition two_power_nat (n:nat) := Zpos (shift_nat n 1).
   Definition two_power_pos (x:positive) := Zpos (shift_pos x 1).
 
-  Lemma two_power_nat_S :
-    forall n:nat, two_power_nat (S n) = 2 * two_power_nat n.
+  Definition two_p (x:Z) :=
+    match x with
+      | Z0 => 1
+      | Zpos y => two_power_pos y
+      | Zneg y => 0
+    end.
+
+  (** Equivalence with notions defined in BinInt *)
+
+  Lemma shift_nat_equiv n p : shift_nat n p = Pos.shiftl_nat p n.
   Proof. reflexivity. Qed.
 
-  Lemma shift_nat_plus :
-    forall (n m:nat) (x:positive),
-      shift_nat (n + m) x = shift_nat n (shift_nat m x).
+  Lemma shift_pos_equiv n p : shift_pos n p = Pos.shiftl p (Npos n).
+  Proof. reflexivity. Qed.
+
+  Lemma shift_equiv n p : 0<=n -> Zpos (shift n p) = Z.shiftl (Zpos p) n.
   Proof.
-    intros; apply iter_nat_plus.
+   destruct n.
+   - trivial.
+   - simpl; intros. now apply Pos.iter_swap_gen.
+   - now destruct 1.
   Qed.
 
-  Theorem shift_nat_correct :
-    forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
+  Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
   Proof.
-    unfold shift_nat; induction n.
-    trivial.
-    intros x. simpl.
-    change (Zpower_nat 2 (S n)) with (2 * Zpower_nat 2 n).
-    now rewrite <- Zmult_assoc, <- IHn.
+   induction n.
+   - trivial.
+   - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
   Qed.
 
-  Theorem two_power_nat_correct :
-    forall n:nat, two_power_nat n = Zpower_nat 2 n.
+  Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p.
   Proof.
-    intro n.
-    unfold two_power_nat.
-    rewrite (shift_nat_correct n).
-    omega.
+   now apply Pos.iter_swap_gen.
   Qed.
 
-  (** Second we show that [two_power_pos] and [two_power_nat] are the same *)
-  Lemma shift_pos_nat :
-    forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x.
+  Lemma two_p_equiv x : two_p x = 2 ^ x.
   Proof.
-    unfold shift_pos, shift_nat. intros. apply iter_nat_of_P.
+   destruct x; trivial. apply two_power_pos_equiv.
   Qed.
 
-  Lemma two_power_pos_nat :
-    forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).
+  (** Properties of these old versions of powers of two *)
+
+  Lemma two_power_nat_S n : two_power_nat (S n) = 2 * two_power_nat n.
+  Proof. reflexivity. Qed.
+
+  Lemma shift_nat_plus n m x :
+    shift_nat (n + m) x = shift_nat n (shift_nat m x).
   Proof.
-    intro. unfold two_power_pos, two_power_nat.
-    f_equal. apply shift_pos_nat.
+   apply iter_nat_plus.
   Qed.
 
-  (** Then we deduce that [two_power_pos] is also correct *)
-
-  Theorem shift_pos_correct :
-    forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
+  Theorem shift_nat_correct n x :
+    Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
   Proof.
-    intros.
-    rewrite (shift_pos_nat p x).
-    rewrite (Zpower_pos_nat 2 p).
-    apply shift_nat_correct.
+   induction n.
+   - trivial.
+   - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
   Qed.
 
-  Theorem two_power_pos_correct :
-    forall x:positive, two_power_pos x = Zpower_pos 2 x.
+  Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n.
   Proof.
-    intro.
-    rewrite two_power_pos_nat.
-    rewrite Zpower_pos_nat.
-    apply two_power_nat_correct.
+   now rewrite two_power_nat_equiv, Zpower_nat_Z.
   Qed.
 
-  (** Some consequences *)
+  Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x.
+  Proof.
+   apply Pos2Nat.inj_iter.
+  Qed.
 
-  Theorem two_power_pos_is_exp :
-    forall x y:positive,
-      two_power_pos (x + y) = two_power_pos x * two_power_pos y.
+  Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p).
   Proof.
-    intros. rewrite 3 two_power_pos_correct. apply Zpower_pos_is_exp.
+   unfold two_power_pos. now rewrite shift_pos_nat.
   Qed.
 
-  (** The exponentiation [z -> 2^z] for [z] a signed integer.
-      For convenience, we assume that [2^z = 0] for all [z < 0]
-      We could also define a inductive type [Log_result] with
-      3 contructors [ Zero | Pos positive -> | minus_infty]
-      but it's more complexe and not so useful. *)
+  Theorem shift_pos_correct p x :
+    Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
+  Proof.
+   now rewrite shift_pos_nat, Zpower_pos_nat, shift_nat_correct.
+  Qed.
 
-  Definition two_p (x:Z) :=
-    match x with
-      | Z0 => 1
-      | Zpos y => two_power_pos y
-      | Zneg y => 0
-    end.
+  Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x.
+  Proof.
+   apply two_power_pos_equiv.
+  Qed.
 
-  Lemma two_p_correct : forall x, two_p x = 2^x.
+  Theorem two_power_pos_is_exp x y :
+   two_power_pos (x + y) = two_power_pos x * two_power_pos y.
   Proof.
-   intros [|p|p]; trivial. apply two_power_pos_correct.
+    rewrite 3 two_power_pos_equiv. now apply (Z.pow_add_r 2 (Zpos x) (Zpos y)).
   Qed.
 
-  Theorem two_p_is_exp :
-    forall x y, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
+  Lemma two_p_correct x : two_p x = 2^x.
+  Proof (two_p_equiv x).
+
+  Theorem two_p_is_exp x y :
+    0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
   Proof.
-   intros. rewrite 3 two_p_correct. apply Z.pow_add_r; auto with zarith.
+    rewrite !two_p_equiv. apply Z.pow_add_r.
   Qed.
 
-  Lemma two_p_gt_ZERO : forall x, 0 <= x -> two_p x > 0.
+  Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0.
   Proof.
-   intros. rewrite two_p_correct. now apply Zlt_gt, Z.pow_pos_nonneg.
+   Z.swap_greater. rewrite two_p_equiv. now apply Z.pow_pos_nonneg.
   Qed.
 
-  Lemma two_p_S : forall x, 0 <= x -> two_p (Zsucc x) = 2 * two_p x.
+  Lemma two_p_S x : 0 <= x -> two_p (Z.succ x) = 2 * two_p x.
   Proof.
-   intros. rewrite 2 two_p_correct. now apply Z.pow_succ_r.
+   rewrite !two_p_equiv. now apply Z.pow_succ_r.
   Qed.
 
-  Lemma two_p_pred : forall x, 0 <= x -> two_p (Zpred x) < two_p x.
+  Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x.
   Proof.
-   intros. rewrite 2 two_p_correct.
-   apply Z.pow_lt_mono_r; auto with zarith.
+   rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith.
   Qed.
 
 End Powers_of_2.
@@ -214,100 +230,88 @@ Section power_div_with_rest.
 
   (** * Division by a power of two. *)
 
-  (** To [n:Z] and [p:positive], [q],[r] are associated such that
-      [n = 2^p.q + r] and [0 <= r < 2^p] *)
+  (** To [x:Z] and [p:positive], [q],[r] are associated such that
+      [x = 2^p.q + r] and [0 <= r < 2^p] *)
 
-  (** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
+  (** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<=r<d /\ 0<=r'<d'] *)
   Definition Zdiv_rest_aux (qrd:Z * Z * Z) :=
-    let (qr, d) := qrd in
-      let (q, r) := qr in
-	(match q with
-	   | Z0 => (0, r)
-	   | Zpos xH => (0, d + r)
-	   | Zpos (xI n) => (Zpos n, d + r)
-	   | Zpos (xO n) => (Zpos n, r)
-	   | Zneg xH => (-1, d + r)
-	   | Zneg (xI n) => (Zneg n - 1, d + r)
-	   | Zneg (xO n) => (Zneg n, r)
-	 end, 2 * d).
+    let '(q,r,d) := qrd in
+      (match q with
+	 | Z0 => (0, r)
+	 | Zpos xH => (0, d + r)
+	 | Zpos (xI n) => (Zpos n, d + r)
+	 | Zpos (xO n) => (Zpos n, r)
+	 | Zneg xH => (-1, d + r)
+	 | Zneg (xI n) => (Zneg n - 1, d + r)
+	 | Zneg (xO n) => (Zneg n, r)
+       end, 2 * d).
 
   Definition Zdiv_rest (x:Z) (p:positive) :=
-    let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in qr.
+    let (qr, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in qr.
 
-  Lemma Zdiv_rest_correct1 :
-    forall (x:Z) (p:positive),
-      let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in d = two_power_pos p.
+  Lemma Zdiv_rest_correct1 (x:Z) (p:positive) :
+    let (_, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    d = two_power_pos p.
   Proof.
-    intros x p; rewrite (iter_nat_of_P p _ Zdiv_rest_aux (x, 0, 1));
-      rewrite (two_power_pos_nat p); elim (nat_of_P p);
-	simpl in |- *;
-	  [ trivial with zarith
-	    | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *;
-	      elim (iter_nat n _ Zdiv_rest_aux (x, 0, 1));
-		destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z);
-		  assumption ].
+   rewrite Pos2Nat.inj_iter, two_power_pos_nat.
+   induction (Pos.to_nat p); simpl; trivial.
+   destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d).
+   unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
   Qed.
 
-  Lemma Zdiv_rest_correct2 :
-    forall (x:Z) (p:positive),
-      let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in
-	let (q, r) := qr in x = q * d + r /\ 0 <= r < d.
+  Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
+    let '(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    x = q * d + r /\ 0 <= r < d.
   Proof.
-    intros;
-      apply iter_pos_invariant with
-	(f := Zdiv_rest_aux)
-	(Inv := fun qrd:Z * Z * Z =>
-          let (qr, d) := qrd in
-            let (q, r) := qr in x = q * d + r /\ 0 <= r < d);
-	[ intro x0; elim x0; intro y0; elim y0; intros q r d;
-	  unfold Zdiv_rest_aux in |- *; elim q;
-	    [ omega
-	      | destruct p0;
-		[ rewrite BinInt.Zpos_xI; intro; elim H; intros; split;
-		  [ rewrite H0; rewrite Zplus_assoc; rewrite Zmult_plus_distr_l;
-		    rewrite Zmult_1_l; rewrite Zmult_assoc;
-		      rewrite (Zmult_comm (Zpos p0) 2); apply refl_equal
-		    | omega ]
-		  | rewrite BinInt.Zpos_xO; intro; elim H; intros; split;
-		    [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zpos p0) 2);
-		      apply refl_equal
-		      | omega ]
-		  | omega ]
-	      | destruct p0;
-		[ rewrite BinInt.Zneg_xI; unfold Zminus in |- *; intro; elim H; intros;
-		  split;
-		    [ rewrite H0; rewrite Zplus_assoc;
-		      apply f_equal with (f := fun z:Z => z + r);
-			do 2 rewrite Zmult_plus_distr_l; rewrite Zmult_assoc;
-			  rewrite (Zmult_comm (Zneg p0) 2); rewrite <- Zplus_assoc;
-			    apply f_equal with (f := fun z:Z => 2 * Zneg p0 * d + z);
-			      omega
-		      | omega ]
-		  | rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros;
-		    split;
-		      [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2);
-			apply refl_equal
-			| omega ]
-		  | omega ] ]
-	  | omega ].
+   apply Pos.iter_invariant; [|omega].
+   intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux.
+   destruct q as [ |[q|q| ]|[q|q| ]]; try omega.
+   - rewrite Z.pos_xI, Z.mul_add_distr_r in H.
+     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+   - rewrite Z.pos_xO in H.
+     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+   - rewrite Z.neg_xI, Z.mul_sub_distr_r in H.
+     rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega.
+   - rewrite Z.neg_xO in H.
+     rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
   Qed.
 
+  (** Old-style rich specification by proof of existence *)
+
   Inductive Zdiv_rest_proofs (x:Z) (p:positive) : Set :=
     Zdiv_rest_proof :
     forall q r:Z,
       x = q * two_power_pos p + r ->
       0 <= r -> r < two_power_pos p -> Zdiv_rest_proofs x p.
 
-  Lemma Zdiv_rest_correct : forall (x:Z) (p:positive), Zdiv_rest_proofs x p.
+  Lemma Zdiv_rest_correct (x:Z) (p:positive) : Zdiv_rest_proofs x p.
   Proof.
-    intros x p.
     generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-    elim (iter_pos p _ Zdiv_rest_aux (x, 0, 1)).
-    simple induction a.
-    intros.
-    elim H; intros H1 H2; clear H.
-    rewrite H0 in H1; rewrite H0 in H2; elim H2; intros;
-      apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
+    destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+    intros (H1,(H2,H3)) ->. now exists q r.
+  Qed.
+
+  (** Direct correctness of [Zdiv_rest] *)
+
+  Lemma Zdiv_rest_ok x p :
+    let (q,r) := Zdiv_rest x p in
+    x = q * 2^(Zpos p) + r /\ 0 <= r < 2^(Zpos p).
+  Proof.
+   unfold Zdiv_rest.
+   generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
+   destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+   intros H ->. now rewrite two_power_pos_equiv in H.
+  Qed.
+
+  (** Equivalence with [Z.shiftr] *)
+
+  Lemma Zdiv_rest_shiftr x p :
+   fst (Zdiv_rest x p) = Z.shiftr x (Zpos p).
+  Proof.
+   generalize (Zdiv_rest_ok x p). destruct (Zdiv_rest x p) as (q,r).
+   intros (H,H'). simpl.
+   rewrite Z.shiftr_div_pow2 by easy.
+   apply Z.div_unique_pos with r; trivial. now rewrite Z.mul_comm.
   Qed.
 
 End power_div_with_rest.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 9c1e69ac7..178111cdf 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -14,6 +14,7 @@ Zcomplements.vo
 Zdiv.vo
 Zeven.vo
 Zgcd_alt.vo
+Zpow_alt.vo
 Zhints.vo
 Zlogarithm.vo
 Zmax.vo