1 files changed, 192 insertions, 235 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 038748b5..5052d01a 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -1,79 +1,89 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(*i $Id: Zpower.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-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] *)
 
-Infix "^" := Zpower : Z_scope.
+(** 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 [[n:positive](Zpower_pos z n)] is a morphism
-   for [add : 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 (nat_of_P_plus_morphism 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.
@@ -81,178 +91,137 @@ Section Powers_of_2.
   (** * Powers of 2 *)
 
   (** For the powers of two, that will be widely used, a more direct
-      calculus is possible. We will also prove some properties such
-      as [(x:positive) x < 2^x] that are true for all integers bigger
-      than 2 but more difficult to prove and useless. *)
-
-  (** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
+      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_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.
-    intro; simpl in |- *; apply refl_equal.
+   destruct n.
+   - trivial.
+   - simpl; intros. now apply Pos.iter_swap_gen.
+   - now destruct 1.
   Qed.
 
-  Lemma shift_nat_plus :
-    forall (n m:nat) (x:positive),
-      shift_nat (n + m) x = shift_nat n (shift_nat m x).
+  Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
   Proof.
-    intros; unfold shift_nat in |- *; apply iter_nat_plus.
+   induction n.
+   - trivial.
+   - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
   Qed.
 
-  Theorem shift_nat_correct :
-    forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
+  Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p.
   Proof.
-    unfold shift_nat in |- *; simple induction n;
-      [ simpl in |- *; trivial with zarith
-	| intros; replace (Zpower_nat 2 (S n0)) with (2 * Zpower_nat 2 n0);
-	  [ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity
-	    | auto with zarith ] ].
+   now apply Pos.iter_swap_gen.
   Qed.
 
-  Theorem two_power_nat_correct :
-    forall n:nat, two_power_nat n = Zpower_nat 2 n.
+  Lemma two_p_equiv x : two_p x = 2 ^ x.
   Proof.
-    intro n.
-    unfold two_power_nat in |- *.
-    rewrite (shift_nat_correct n).
-    omega.
+   destruct x; trivial. apply two_power_pos_equiv.
   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.
+  (** 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.
-    unfold shift_pos in |- *.
-    unfold shift_nat in |- *.
-    intros; apply iter_nat_of_P.
+   apply iter_nat_plus.
   Qed.
 
-  Lemma two_power_pos_nat :
-    forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).
+  Theorem shift_nat_correct n x :
+    Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
   Proof.
-    intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *.
-    apply f_equal with (f := Zpos).
-    apply shift_pos_nat.
+   induction n.
+   - trivial.
+   - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
   Qed.
 
-  (** Then we deduce that [two_power_pos] is also correct *)
+  Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n.
+  Proof.
+   now rewrite two_power_nat_equiv, Zpower_nat_Z.
+  Qed.
 
-  Theorem shift_pos_correct :
-    forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
+  Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x.
   Proof.
-    intros.
-    rewrite (shift_pos_nat p x).
-    rewrite (Zpower_pos_nat 2 p).
-    apply shift_nat_correct.
+   apply Pos2Nat.inj_iter.
   Qed.
 
-  Theorem two_power_pos_correct :
-    forall x:positive, two_power_pos x = Zpower_pos 2 x.
+  Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p).
   Proof.
-    intro.
-    rewrite two_power_pos_nat.
-    rewrite Zpower_pos_nat.
-    apply two_power_nat_correct.
+   unfold two_power_pos. now rewrite shift_pos_nat.
   Qed.
 
-  (** Some consequences *)
+  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.
 
-  Theorem two_power_pos_is_exp :
-    forall x y:positive,
-      two_power_pos (x + y) = two_power_pos x * two_power_pos y.
+  Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x.
   Proof.
-    intros.
-    rewrite (two_power_pos_correct (x + y)).
-    rewrite (two_power_pos_correct x).
-    rewrite (two_power_pos_correct y).
-    apply Zpower_pos_is_exp.
+   apply two_power_pos_equiv.
   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 two_power_pos_is_exp x y :
+   two_power_pos (x + y) = two_power_pos x * two_power_pos y.
+  Proof.
+    rewrite 3 two_power_pos_equiv. now apply (Z.pow_add_r 2 (Zpos x) (Zpos y)).
+  Qed.
 
-  Definition two_p (x:Z) :=
-    match x with
-      | Z0 => 1
-      | Zpos y => two_power_pos y
-      | Zneg y => 0
-    end.
+  Lemma two_p_correct x : two_p x = 2^x.
+  Proof (two_p_equiv x).
 
-  Theorem two_p_is_exp :
-    forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
+  Theorem two_p_is_exp x y :
+    0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
   Proof.
-    simple induction x;
-      [ simple induction y; simpl in |- *; auto with zarith
-	| simple induction y;
-	  [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1);
-	    rewrite (Zmult_1_l (two_power_pos p)); auto with zarith
-	    | unfold Zplus in |- *; unfold two_p in |- *; intros;
-	      apply two_power_pos_is_exp
-	    | intros; unfold Zle in H0; unfold Zcompare in H0;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ]
-	| simple induction y;
-	  [ simpl in |- *; auto with zarith
-	    | intros; unfold Zle in H; unfold Zcompare in H;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith
-	    | intros; unfold Zle in H; unfold Zcompare in H;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ].
+    rewrite !two_p_equiv. apply Z.pow_add_r.
   Qed.
 
-  Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0.
+  Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0.
   Proof.
-    simple induction x; intros;
-      [ simpl in |- *; omega
-	| simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0
-	| absurd (0 <= Zneg p);
-	  [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *;
-	    do 2 unfold not in |- *; auto with zarith
-	    | assumption ] ].
+   Z.swap_greater. rewrite two_p_equiv. now apply Z.pow_pos_nonneg.
   Qed.
 
-  Lemma two_p_S : forall x:Z, 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; unfold Zsucc in |- *.
-    rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)).
-    apply Zmult_comm.
+   rewrite !two_p_equiv. now apply Z.pow_succ_r.
   Qed.
 
-  Lemma two_p_pred : forall x:Z, 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; apply natlike_ind with (P := fun x:Z => two_p (Zpred x) < two_p x);
-      [ simpl in |- *; unfold Zlt in |- *; auto with zarith
-	| intros; elim (Zle_lt_or_eq 0 x0 H0);
-	  [ intros;
-	    replace (two_p (Zpred (Zsucc x0))) with (two_p (Zsucc (Zpred x0)));
-	      [ rewrite (two_p_S (Zpred x0));
-		[ rewrite (two_p_S x0); [ omega | assumption ]
-		  | apply Zorder.Zlt_0_le_0_pred; assumption ]
-		| rewrite <- (Zsucc_pred x0); rewrite <- (Zpred_succ x0);
-		  trivial with zarith ]
-	    | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *;
-	      auto with zarith ]
-	| assumption ].
+   rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith.
   Qed.
 
-  Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y.
-    intros; omega. Qed.
-
-  End Powers_of_2.
+End Powers_of_2.
 
 Hint Resolve two_p_gt_ZERO: zarith.
 Hint Immediate two_p_pred two_p_S: zarith.
@@ -261,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 (Z * Z * Z) 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 (Z * Z * Z) 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.