Move Z definitions out of Integers and into Zbits

The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size.  These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.

This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.

13 files changed, 1031 insertions, 884 deletions

diff --git a/Makefile b/Makefile
index 5a9701aa..7b1d3a76 100644
--- a/Makefile
+++ b/Makefile
@@ -53,7 +53,7 @@ FLOCQ=\
 # General-purpose libraries (in lib/)
 
 VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
-  Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
+  Iteration.v Zbits.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v
 
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 98cd5eea..edf35bb8 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -355,7 +356,7 @@ Proof.
   rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem.
   apply Int.same_bits_eq; intros.
   rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto.
-  rewrite Int.Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16.
+  rewrite Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16.
   destruct (zlt i 16).
   rewrite andb_true_r, orb_false_r; auto.
   rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 692b4f9b..5d19e8f6 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import IntvSets.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -300,13 +301,13 @@ Proof.
   rewrite Int.bits_ror.
   replace (((i - Int.unsigned amount) mod Int.zwordsize + Int.unsigned amount)
    mod Int.zwordsize) with i. auto.
-  apply Int.eqmod_small_eq with Int.zwordsize; auto.
-  apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
-  apply Int.eqmod_refl2; omega.
-  eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto.
-  apply Int.eqmod_add.
-  apply Int.eqmod_mod; auto.
-  apply Int.eqmod_refl.
+  apply eqmod_small_eq with Int.zwordsize; auto.
+  apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
+  apply eqmod_refl2; omega.
+  eapply eqmod_trans. 2: apply eqmod_mod; auto.
+  apply eqmod_add.
+  apply eqmod_mod; auto.
+  apply eqmod_refl.
   apply Z_mod_lt; auto.
   apply Z_mod_lt; auto.
 Qed.
@@ -324,7 +325,7 @@ Qed.
 
 Lemma eqmod_iagree:
   forall m x y,
-  Int.eqmod (two_p (Int.size m)) x y ->
+  eqmod (two_p (Int.size m)) x y ->
   iagree (Int.repr x) (Int.repr y) m.
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
@@ -333,7 +334,7 @@ Proof.
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
-  eapply Int.same_bits_eqmod; eauto. omega.
+  eapply same_bits_eqmod; eauto. omega.
   assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega).
   congruence.
 Qed.
@@ -343,13 +344,13 @@ Definition complete_mask (m: int) := Int.zero_ext (Int.size m) Int.mone.
 Lemma iagree_eqmod:
   forall x y m,
   iagree x y (complete_mask m) ->
-  Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
+  eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
   assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
-  apply Int.eqmod_same_bits. intros. apply H. omega.
+  apply eqmod_same_bits. intros. apply H. omega.
   unfold complete_mask. rewrite Int.bits_zero_ext by omega.
   rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto.
 Qed.
@@ -362,7 +363,7 @@ Proof.
 + assert (Int.unsigned m <> 0).
   { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. }
   assert (0 < Int.size m).
-  { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. }
+  { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. }
   generalize (Int.size_range m); intros.
   f_equal. apply Int.bits_size_4. tauto.
   rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega.
@@ -610,7 +611,7 @@ Proof.
   unfold modarith; intros. destruct x; simpl in *.
 - auto.
 - unfold Val.add; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_add; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -626,7 +627,7 @@ Lemma mul_sound:
 Proof.
   unfold mul, add; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto.
+- unfold Val.mul; InvAgree. apply eqmod_iagree. apply eqmod_mult; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -638,7 +639,7 @@ Proof.
   intros; destruct x; simpl in *.
 - auto.
 - unfold Val.neg; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_neg. apply iagree_eqmod; auto.
 - inv H; simpl; auto.
 Qed.
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index e660677a..f4ff2c86 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import Zquot Coqlib.
+Require Import Zquot Coqlib Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
@@ -378,7 +378,7 @@ Qed.
 Remark int64_shr'_div_two_p:
   forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shr'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Lemma divls_mul_shift_gen:
@@ -453,7 +453,7 @@ Qed.
 Remark int64_shru'_div_two_p:
   forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shru'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Theorem divlu_mul_shift:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 47b87bfb..3ba2a35b 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -11,7 +11,7 @@
 (* *********************************************************************)
 
 Require Import FunInd.
-Require Import Zwf Coqlib Maps Integers Floats Lattice.
+Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Events.
 Require Import Registers RTL.
@@ -1670,7 +1670,7 @@ Proof.
   assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
   {
     intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va.
-    unfold usize, Int.size. apply Int.Zsize_monotone.
+    unfold usize, Int.size. apply Zsize_monotone.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
diff --git a/common/Memdata.v b/common/Memdata.v
index c53f0e5d..7144d72c 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -17,6 +17,7 @@
 (** In-memory representation of values. *)
 
 Require Import Coqlib.
+Require Import Zbits.
 Require Archi.
 Require Import AST.
 Require Import Integers.
@@ -272,7 +273,7 @@ Qed.
 
 Lemma bytes_of_int_mod:
   forall n x y,
-  Int.eqmod (two_p (Z.of_nat n * 8)) x y ->
+  eqmod (two_p (Z.of_nat n * 8)) x y ->
   bytes_of_int n x = bytes_of_int n y.
 Proof.
   induction n.
@@ -284,7 +285,7 @@ Proof.
   intro EQM.
   simpl; decEq.
   apply Byte.eqm_samerepr. red.
-  eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r.
+  eapply eqmod_divides; eauto. apply Z.divide_factor_r.
   apply IHn.
   destruct EQM as [k EQ]. exists k. rewrite EQ.
   rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega.
@@ -292,7 +293,7 @@ Qed.
 
 Lemma encode_int_8_mod:
   forall x y,
-  Int.eqmod (two_p 8) x y ->
+  eqmod (two_p 8) x y ->
   encode_int 1%nat x = encode_int 1%nat y.
 Proof.
   intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
@@ -300,7 +301,7 @@ Qed.
 
 Lemma encode_int_16_mod:
   forall x y,
-  Int.eqmod (two_p 16) x y ->
+  eqmod (two_p 16) x y ->
   encode_int 2%nat x = encode_int 2%nat y.
 Proof.
   intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
diff --git a/lib/Floats.v b/lib/Floats.v
index f93505fc..21d09a5e 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -16,8 +16,7 @@
 
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
-Require Import Coqlib.
-Require Import Integers.
+Require Import Coqlib Zbits Integers.
 (*From Flocq*)
 Require Import Binary Bits Core.
 Require Import Fappli_IEEE_extra.
@@ -1356,9 +1355,9 @@ Proof.
   rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and.
   change (Int64.unsigned (Int64.repr 2047)) with 2047.
   change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega.
-  rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq.
+  rewrite Int64.unsigned_repr. apply eqmod_mod_eq.
   apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega.
-  apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned.
+  apply eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned.
   exists (2^(64-11)); auto.
   exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto.
   assert (2^11 < Int64.max_unsigned) by (compute; auto). omega.
diff --git a/lib/Integers.v b/lib/Integers.v
index 64263b97..8f528079 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -16,7 +16,7 @@
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
 Require Import Eqdep_dec Zquot Zwf.
-Require Import Coqlib.
+Require Import Coqlib Zbits.
 Require Archi.
 
 (** * Comparisons *)
@@ -91,6 +91,8 @@ Proof.
   generalize modulus_gt_one; omega.
 Qed.
 
+Hint Resolve modulus_pos: ints.
+
 (** * Representation of machine integers *)
 
 (** A machine integer (type [int]) is represented as a Coq arbitrary-precision
@@ -101,17 +103,6 @@ Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.
 
 (** Fast normalization modulo [2^wordsize] *)
 
-Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z :=
-  match n with
-  | O => 0
-  | S m =>
-      match p with
-      | xH => 1
-      | xO q => Z.double (P_mod_two_p q m)
-      | xI q => Z.succ_double (P_mod_two_p q m)
-      end
-  end.
-
 Definition Z_mod_modulus (x: Z) : Z :=
   match x with
   | Z0 => 0
@@ -119,51 +110,9 @@ Definition Z_mod_modulus (x: Z) : Z :=
   | Zneg p => let r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r
   end.
 
-Lemma P_mod_two_p_range:
-  forall n p, 0 <= P_mod_two_p p n < two_power_nat n.
-Proof.
-  induction n; simpl; intros.
-  - rewrite two_power_nat_O. omega.
-  - rewrite two_power_nat_S. destruct p.
-    + generalize (IHn p). rewrite Z.succ_double_spec. omega.
-    + generalize (IHn p). rewrite Z.double_spec. omega.
-    + generalize (two_power_nat_pos n). omega.
-Qed.
-
-Lemma P_mod_two_p_eq:
-  forall n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).
-Proof.
-  assert (forall n p, exists y, Zpos p = y * two_power_nat n + P_mod_two_p p n).
-  {
-    induction n; simpl; intros.
-    - rewrite two_power_nat_O. exists (Zpos p). ring.
-    - rewrite two_power_nat_S. destruct p.
-      + destruct (IHn p) as [y EQ]. exists y.
-        change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ.
-        rewrite Z.succ_double_spec. ring.
-      + destruct (IHn p) as [y EQ]. exists y.
-        change (Zpos p~0) with (2 * Zpos p). rewrite EQ.
-        rewrite (Z.double_spec (P_mod_two_p p n)). ring.
-      + exists 0; omega.
-  }
-  intros.
-  destruct (H n p) as [y EQ].
-  symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range.
-Qed.
-
 Lemma Z_mod_modulus_range:
   forall x, 0 <= Z_mod_modulus x < modulus.
-Proof.
-  intros; unfold Z_mod_modulus.
-  destruct x.
-  - generalize modulus_pos; intuition.
-  - apply P_mod_two_p_range.
-  - set (r := P_mod_two_p p wordsize).
-    assert (0 <= r < modulus) by apply P_mod_two_p_range.
-    destruct (zeq r 0).
-    + generalize modulus_pos; intuition.
-    + Psatz.lia.
-Qed.
+Proof (Z_mod_two_p_range wordsize).
 
 Lemma Z_mod_modulus_range':
   forall x, -1 < Z_mod_modulus x < modulus.
@@ -173,22 +122,7 @@ Qed.
 
 Lemma Z_mod_modulus_eq:
   forall x, Z_mod_modulus x = x mod modulus.
-Proof.
-  intros. unfold Z_mod_modulus. destruct x.
-  - rewrite Zmod_0_l. auto.
-  - apply P_mod_two_p_eq.
-  - generalize (P_mod_two_p_range wordsize p) (P_mod_two_p_eq wordsize p).
-    fold modulus. intros A B.
-    exploit (Z_div_mod_eq (Zpos p) modulus). apply modulus_pos. intros C.
-    set (q := Zpos p / modulus) in *.
-    set (r := P_mod_two_p p wordsize) in *.
-    rewrite <- B in C.
-    change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0).
-    + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia.
-      intuition.
-    + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia.
-      intuition.
-Qed.
+Proof (Z_mod_two_p_eq wordsize).
 
 (** The [unsigned] and [signed] functions return the Coq integer corresponding
   to the given machine integer, interpreted as unsigned or signed
@@ -323,54 +257,11 @@ Definition shr_carry (x y: int) : int :=
 
 (** Zero and sign extensions *)
 
-Definition Zshiftin (b: bool) (x: Z) : Z :=
-  if b then Z.succ_double x else Z.double x.
-
-(** In pseudo-code:
-<<
-    Fixpoint Zzero_ext (n: Z) (x: Z) : Z :=
-      if zle n 0 then
-        0
-      else
-        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
-    Fixpoint Zsign_ext (n: Z) (x: Z) : Z :=
-      if zle n 1 then
-        if Z.odd x then -1 else 0
-      else
-        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
->>
-  We encode this [nat]-like recursion using the [Z.iter] iteration
-  function, in order to make the [Zzero_ext] and [Zsign_ext]
-  functions efficiently executable within Coq.
-*)
-
-Definition Zzero_ext (n: Z) (x: Z) : Z :=
-  Z.iter n
-    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
-    (fun x => 0)
-    x.
-
-Definition Zsign_ext (n: Z) (x: Z) : Z :=
-  Z.iter (Z.pred n)
-    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
-    (fun x => if Z.odd x then -1 else 0)
-    x.
-
 Definition zero_ext (n: Z) (x: int) : int := repr (Zzero_ext n (unsigned x)).
-
 Definition sign_ext (n: Z) (x: int) : int := repr (Zsign_ext n (unsigned x)).
 
 (** Decomposition of a number as a sum of powers of two. *)
 
-Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
-  match n with
-  | O => nil
-  | S m =>
-      if Z.odd x
-      then i :: Z_one_bits m (Z.div2 x) (i+1)
-      else Z_one_bits m (Z.div2 x) (i+1)
-  end.
-
 Definition one_bits (x: int) : list int :=
   List.map repr (Z_one_bits wordsize (unsigned x) 0).
 
@@ -503,101 +394,7 @@ Qed.
 
 (** ** Modulo arithmetic *)
 
-(** We define and state properties of equality and arithmetic modulo a
-  positive integer. *)
-
-Section EQ_MODULO.
-
-Variable modul: Z.
-Hypothesis modul_pos: modul > 0.
-
-Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.
-
-Lemma eqmod_refl: forall x, eqmod x x.
-Proof.
-  intros; red. exists 0. omega.
-Qed.
-
-Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
-Proof.
-  intros. subst y. apply eqmod_refl.
-Qed.
-
-Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
-Proof.
-  intros x y [k EQ]; red. exists (-k). subst x. ring.
-Qed.
-
-Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
-Proof.
-  intros x y z [k1 EQ1] [k2 EQ2]; red.
-  exists (k1 + k2). subst x; subst y. ring.
-Qed.
-
-Lemma eqmod_small_eq:
-  forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
-Proof.
-  intros x y [k EQ] I1 I2.
-  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
-  rewrite (Z.div_small x modul I1) in H. subst k. omega.
-Qed.
-
-Lemma eqmod_mod_eq:
-  forall x y, eqmod x y -> x mod modul = y mod modul.
-Proof.
-  intros x y [k EQ]. subst x.
-  rewrite Z.add_comm. apply Z_mod_plus. auto.
-Qed.
-
-Lemma eqmod_mod:
-  forall x, eqmod x (x mod modul).
-Proof.
-  intros; red. exists (x / modul).
-  rewrite Z.mul_comm. apply Z_div_mod_eq. auto.
-Qed.
-
-Lemma eqmod_add:
-  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
-Proof.
-  intros a b c d [k1 EQ1] [k2 EQ2]; red.
-  subst a; subst c. exists (k1 + k2). ring.
-Qed.
-
-Lemma eqmod_neg:
-  forall x y, eqmod x y -> eqmod (-x) (-y).
-Proof.
-  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
-Qed.
-
-Lemma eqmod_sub:
-  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
-Proof.
-  intros a b c d [k1 EQ1] [k2 EQ2]; red.
-  subst a; subst c. exists (k1 - k2). ring.
-Qed.
-
-Lemma eqmod_mult:
-  forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
-Proof.
-  intros a b c d [k1 EQ1] [k2 EQ2]; red.
-  subst a; subst b.
-  exists (k1 * k2 * modul + c * k2 + k1 * d).
-  ring.
-Qed.
-
-End EQ_MODULO.
-
-Lemma eqmod_divides:
-  forall n m x y, eqmod n x y -> Z.divide m n -> eqmod m x y.
-Proof.
-  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
-  exists (k1*k2). rewrite <- Z.mul_assoc. rewrite <- EQ2. auto.
-Qed.
-
-(** We then specialize these definitions to equality modulo
-  $2^{wordsize}$ #2<sup>wordsize</sup>#. *)
-
-Hint Resolve modulus_pos: ints.
+(** [eqm] is equality modulo $2^{wordsize}$ #2<sup>wordsize</sup>#. *)
 
 Definition eqm := eqmod modulus.
 
@@ -643,6 +440,19 @@ Lemma eqm_mult:
 Proof (eqmod_mult modulus).
 Hint Resolve eqm_mult: ints.
 
+Lemma eqm_same_bits:
+  forall x y,
+  (forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) ->
+  eqm x y.
+Proof (eqmod_same_bits wordsize).
+
+Lemma same_bits_eqm:
+  forall x y i,
+  eqm x y ->
+  0 <= i < zwordsize ->
+  Z.testbit x i = Z.testbit y i.
+Proof (same_bits_eqmod wordsize).
+
 (** ** Properties of the coercions between [Z] and [int] *)
 
 Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
@@ -1304,298 +1114,6 @@ Qed.
 
 (** ** Bit-level properties *)
 
-(** ** Properties of bit-level operations over [Z] *)
-
-Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
-Proof Z.testbit_0_l.
-
-Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
-Proof.
-  intros. destruct n; simpl; auto.
-Qed.
-
-Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
-Proof.
-  intros. destruct n; simpl; auto.
-Qed.
-
-Remark Zshiftin_spec:
-  forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0).
-Proof.
-  unfold Zshiftin; intros. destruct b.
-  - rewrite Z.succ_double_spec. omega.
-  - rewrite Z.double_spec. omega.
-Qed.
-
-Remark Zshiftin_inj:
-  forall b1 x1 b2 x2,
-  Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2.
-Proof.
-  intros. rewrite !Zshiftin_spec in H.
-  destruct b1; destruct b2.
-  split; [auto|omega].
-  omegaContradiction.
-  omegaContradiction.
-  split; [auto|omega].
-Qed.
-
-Remark Zdecomp:
-  forall x, x = Zshiftin (Z.odd x) (Z.div2 x).
-Proof.
-  intros. destruct x; simpl.
-  - auto.
-  - destruct p; auto.
-  - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto.
-Qed.
-
-Remark Ztestbit_shiftin:
-  forall b x n,
-  0 <= n ->
-  Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n).
-Proof.
-  intros. rewrite Zshiftin_spec. destruct (zeq n 0).
-  - subst n. destruct b.
-    + apply Z.testbit_odd_0.
-    + rewrite Z.add_0_r. apply Z.testbit_even_0.
-  - assert (0 <= Z.pred n) by omega.
-    set (n' := Z.pred n) in *.
-    replace n with (Z.succ n') by (unfold n'; omega).
-    destruct b.
-    + apply Z.testbit_odd_succ; auto.
-    + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto.
-Qed.
-
-Remark Ztestbit_shiftin_base:
-  forall b x, Z.testbit (Zshiftin b x) 0 = b.
-Proof.
-  intros. rewrite Ztestbit_shiftin. apply zeq_true. omega.
-Qed.
-
-Remark Ztestbit_shiftin_succ:
-  forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.
-Proof.
-  intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto.
-  omega. omega.
-Qed.
-
-Remark Ztestbit_eq:
-  forall n x, 0 <= n ->
-  Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n).
-Proof.
-  intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto.
-Qed.
-
-Remark Ztestbit_base:
-  forall x, Z.testbit x 0 = Z.odd x.
-Proof.
-  intros. rewrite Ztestbit_eq. apply zeq_true. omega.
-Qed.
-
-Remark Ztestbit_succ:
-  forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.
-Proof.
-  intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto.
-  omega. omega.
-Qed.
-
-Lemma eqmod_same_bits:
-  forall n x y,
-  (forall i, 0 <= i < Z.of_nat n -> Z.testbit x i = Z.testbit y i) ->
-  eqmod (two_power_nat n) x y.
-Proof.
-  induction n; intros.
-  - change (two_power_nat 0) with 1. exists (x-y); ring.
-  - rewrite two_power_nat_S.
-    assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)).
-      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega.
-      omega. omega.
-  destruct H0 as [k EQ].
-  exists k. rewrite (Zdecomp x). rewrite (Zdecomp y).
-  replace (Z.odd y) with (Z.odd x).
-  rewrite EQ. rewrite !Zshiftin_spec. ring.
-  exploit (H 0). rewrite Nat2Z.inj_succ; omega.
-  rewrite !Ztestbit_base. auto.
-Qed.
-
-Lemma eqm_same_bits:
-  forall x y,
-  (forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) ->
-  eqm x y.
-Proof (eqmod_same_bits wordsize).
-
-Lemma same_bits_eqmod:
-  forall n x y i,
-  eqmod (two_power_nat n) x y -> 0 <= i < Z.of_nat n ->
-  Z.testbit x i = Z.testbit y i.
-Proof.
-  induction n; intros.
-  - simpl in H0. omegaContradiction.
-  - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H.
-    rewrite !(Ztestbit_eq i); intuition.
-    destruct H as [k EQ].
-    assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) =
-                 Zshiftin (Z.odd y) (k * two_power_nat n + Z.div2 y)).
-    {
-      rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ.
-      rewrite EQ. rewrite !Zshiftin_spec. ring.
-    }
-    exploit Zshiftin_inj; eauto. intros [A B].
-    destruct (zeq i 0).
-    + auto.
-    + apply IHn. exists k; auto. omega.
-Qed.
-
-Lemma same_bits_eqm:
-  forall x y i,
-  eqm x y ->
-  0 <= i < zwordsize ->
-  Z.testbit x i = Z.testbit y i.
-Proof (same_bits_eqmod wordsize).
-
-Remark two_power_nat_infinity:
-  forall x, 0 <= x -> exists n, x < two_power_nat n.
-Proof.
-  intros x0 POS0; pattern x0; apply natlike_ind; auto.
-  exists O. compute; auto.
-  intros. destruct H0 as [n LT]. exists (S n). rewrite two_power_nat_S.
-  generalize (two_power_nat_pos n). omega.
-Qed.
-
-Lemma equal_same_bits:
-  forall x y,
-  (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
-  x = y.
-Proof.
-  intros.
-  set (z := if zlt x y then y - x else x - y).
-  assert (0 <= z).
-    unfold z; destruct (zlt x y); omega.
-  exploit (two_power_nat_infinity z); auto. intros [n LT].
-  assert (eqmod (two_power_nat n) x y).
-    apply eqmod_same_bits. intros. apply H. tauto.
-  assert (eqmod (two_power_nat n) z 0).
-    unfold z. destruct (zlt x y).
-    replace 0 with (y - y) by omega. apply eqmod_sub. apply eqmod_refl. auto.
-    replace 0 with (x - x) by omega. apply eqmod_sub. apply eqmod_refl. apply eqmod_sym; auto.
-  assert (z = 0).
-    apply eqmod_small_eq with (two_power_nat n). auto. omega. generalize (two_power_nat_pos n); omega.
-  unfold z in H3. destruct (zlt x y); omega.
-Qed.
-
-Lemma Z_one_complement:
-  forall i, 0 <= i ->
-  forall x, Z.testbit (-x-1) i = negb (Z.testbit x i).
-Proof.
-  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
-  intros i IND POS x.
-  rewrite (Zdecomp x). set (y := Z.div2 x).
-  replace (- Zshiftin (Z.odd x) y - 1)
-     with (Zshiftin (negb (Z.odd x)) (- y - 1)).
-  rewrite !Ztestbit_shiftin; auto.
-  destruct (zeq i 0). auto. apply IND. omega.
-  rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring.
-Qed.
-
-Lemma Ztestbit_above:
-  forall n x i,
-  0 <= x < two_power_nat n ->
-  i >= Z.of_nat n ->
-  Z.testbit x i = false.
-Proof.
-  induction n; intros.
-  - change (two_power_nat 0) with 1 in H.
-    replace x with 0 by omega.
-    apply Z.testbit_0_l.
-  - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false.
-    apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H.
-    rewrite Zshiftin_spec in H. destruct (Z.odd x); omega.
-    omega. omega. omega.
-Qed.
-
-Lemma Ztestbit_above_neg:
-  forall n x i,
-  -two_power_nat n <= x < 0 ->
-  i >= Z.of_nat n ->
-  Z.testbit x i = true.
-Proof.
-  intros. set (y := -x-1).
-  assert (Z.testbit y i = false).
-    apply Ztestbit_above with n.
-    unfold y; omega. auto.
-  unfold y in H1. rewrite Z_one_complement in H1.
-  change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto.
-  omega.
-Qed.
-
-Lemma Zsign_bit:
-  forall n x,
-  0 <= x < two_power_nat (S n) ->
-  Z.testbit x (Z.of_nat n) = if zlt x (two_power_nat n) then false else true.
-Proof.
-  induction n; intros.
-  - change (two_power_nat 1) with 2 in H.
-    assert (x = 0 \/ x = 1) by omega.
-    destruct H0; subst x; reflexivity.
-  - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
-    rewrite IHn. rewrite two_power_nat_S.
-    destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec.
-    rewrite zlt_true. auto. destruct (Z.odd x); omega.
-    rewrite zlt_false. auto. destruct (Z.odd x); omega.
-    rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H.
-    rewrite two_power_nat_S in H. destruct (Z.odd x); omega.
-    omega. omega.
-Qed.
-
-Lemma Zshiftin_ind:
-  forall (P: Z -> Prop),
-  P 0 ->
-  (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) ->
-  forall x, 0 <= x -> P x.
-Proof.
-  intros. destruct x.
-  - auto.
-  - induction p.
-    + change (P (Zshiftin true (Z.pos p))). auto.
-    + change (P (Zshiftin false (Z.pos p))). auto.
-    + change (P (Zshiftin true 0)). apply H0. omega. auto.
-  - compute in H1. intuition congruence.
-Qed.
-
-Lemma Zshiftin_pos_ind:
-  forall (P: Z -> Prop),
-  P 1 ->
-  (forall b x, 0 < x -> P x -> P (Zshiftin b x)) ->
-  forall x, 0 < x -> P x.
-Proof.
-  intros. destruct x; simpl in H1; try discriminate.
-  induction p.
-    + change (P (Zshiftin true (Z.pos p))). auto.
-    + change (P (Zshiftin false (Z.pos p))). auto.
-    + auto.
-Qed.
-
-Lemma Ztestbit_le:
-  forall x y,
-  0 <= y ->
-  (forall i, 0 <= i -> Z.testbit x i = true -> Z.testbit y i = true) ->
-  x <= y.
-Proof.
-  intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros.
-  - replace x with 0. omega. apply equal_same_bits; intros.
-    rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto.
-    exploit H; eauto. rewrite Ztestbit_0. auto.
-  - assert (Z.div2 x0 <= x).
-    { apply H0. intros. exploit (H1 (Z.succ i)).
-        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
-    }
-    rewrite (Zdecomp x0). rewrite !Zshiftin_spec.
-    destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega.
-    exploit (H1 0). omega. rewrite Ztestbit_base; auto.
-    rewrite Ztestbit_shiftin_base. congruence.
-Qed.
-
-(** ** Bit-level reasoning over type [int] *)
-
 Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i.
 
 Lemma testbit_repr:
@@ -1894,7 +1412,7 @@ Proof.
   rewrite bits_or; auto. rewrite H0; auto.
 Qed.
 
-(** Properties of bitwise complement.*)
+(** ** Properties of bitwise complement.*)
 
 Theorem not_involutive:
   forall (x: int), not (not x) = x.
@@ -2013,7 +1531,7 @@ Proof.
   rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto.
 Qed.
 
-(** Connections between [add] and bitwise logical operations. *)
+(** ** Connections between [add] and bitwise logical operations. *)
 
 Lemma Z_add_is_or:
   forall i, 0 <= i ->
@@ -2626,56 +2144,7 @@ Proof.
     apply Z.mod_small; auto.
 Qed.
 
-(** ** Properties of [Z_one_bits] and [is_power2]. *)
-
-Fixpoint powerserie (l: list Z): Z :=
-  match l with
-  | nil => 0
-  | x :: xs => two_p x + powerserie xs
-  end.
-
-Lemma Z_one_bits_powerserie:
-  forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
-Proof.
-  assert (forall n x i,
-    0 <= i ->
-    0 <= x < two_power_nat n ->
-    x * two_p i = powerserie (Z_one_bits n x i)).
-  {
-  induction n; intros.
-  simpl. rewrite two_power_nat_O in H0.
-  assert (x = 0) by omega. subst x. omega.
-  rewrite two_power_nat_S in H0. simpl Z_one_bits.
-  rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0.
-  assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))).
-    apply IHn. omega.
-    destruct (Z.odd x); omega.
-  rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ.
-  rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec.
-  destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring.
-  omega. omega.
-  }
-  intros. rewrite <- H. change (two_p 0) with 1. omega.
-  omega. exact H0.
-Qed.
-
-Lemma Z_one_bits_range:
-  forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < zwordsize.
-Proof.
-  assert (forall n x i j,
-    In j (Z_one_bits n x i) -> i <= j < i + Z.of_nat n).
-  {
-  induction n; simpl In.
-  tauto.
-  intros x i j. rewrite Nat2Z.inj_succ.
-  assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)).
-    intros. exploit IHn; eauto. omega.
-  destruct (Z.odd x); simpl.
-  intros [A|B]. subst j. omega. auto.
-  auto.
-  }
-  intros. generalize (H wordsize x 0 i H0). fold zwordsize; omega.
-Qed.
+(** ** Properties of [is_power2]. *)
 
 Lemma is_power2_rng:
   forall n logn,
@@ -2683,7 +2152,7 @@ Lemma is_power2_rng:
   0 <= unsigned logn < zwordsize.
 Proof.
   intros n logn. unfold is_power2.
-  generalize (Z_one_bits_range (unsigned n)).
+  generalize (Z_one_bits_range wordsize (unsigned n)).
   destruct (Z_one_bits wordsize (unsigned n) 0).
   intros; discriminate.
   destruct l.
@@ -2708,14 +2177,14 @@ Lemma is_power2_correct:
   unsigned n = two_p (unsigned logn).
 Proof.
   intros n logn. unfold is_power2.
-  generalize (Z_one_bits_powerserie (unsigned n) (unsigned_range n)).
-  generalize (Z_one_bits_range (unsigned n)).
+  generalize (Z_one_bits_powerserie wordsize (unsigned n) (unsigned_range n)).
+  generalize (Z_one_bits_range wordsize (unsigned n)).
   destruct (Z_one_bits wordsize (unsigned n) 0).
   intros; discriminate.
   destruct l.
   intros. simpl in H0. injection H1; intros; subst logn; clear H1.
   rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
-  auto. omega. elim (H z); intros.
+  auto. omega. elim (H z); change (Z.of_nat wordsize) with zwordsize; intros.
   generalize wordsize_max_unsigned; omega.
   auto with coqlib.
   intros; discriminate.
@@ -2733,28 +2202,6 @@ Proof.
   unfold max_unsigned, modulus. omega.
 Qed.
 
-Remark Z_one_bits_zero:
-  forall n i, Z_one_bits n 0 i = nil.
-Proof.
-  induction n; intros; simpl; auto.
-Qed.
-
-Remark Z_one_bits_two_p:
-  forall n x i,
-  0 <= x < Z.of_nat n ->
-  Z_one_bits n (two_p x) i = (i + x) :: nil.
-Proof.
-  induction n; intros; simpl. simpl in H. omegaContradiction.
-  rewrite Nat2Z.inj_succ in H.
-  assert (x = 0 \/ 0 < x) by omega. destruct H0.
-  subst x; simpl. decEq. omega. apply Z_one_bits_zero.
-  assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)).
-    apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec.
-    rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega.
-  destruct H1 as [A B]; rewrite A; rewrite B.
-  rewrite IHn. f_equal; omega. omega.
-Qed.
-
 Lemma is_power2_two_p:
   forall n, 0 <= n < zwordsize ->
   is_power2 (repr (two_p n)) = Some (repr n).
@@ -2768,19 +2215,6 @@ Qed.
 
 (** Left shifts and multiplications by powers of 2. *)
 
-Lemma Zshiftl_mul_two_p:
-  forall x n, 0 <= n -> Z.shiftl x n = x * two_p n.
-Proof.
-  intros. destruct n; simpl.
-  - omega.
-  - pattern p. apply Pos.peano_ind.
-    + change (two_power_pos 1) with 2. simpl. ring.
-    + intros. rewrite Pos.iter_succ. rewrite H0.
-      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
-      change (two_power_pos 1) with 2. ring.
-  - compute in H. congruence.
-Qed.
-
 Lemma shl_mul_two_p:
   forall x y,
   shl x y = mul x (repr (two_p (unsigned y))).
@@ -2840,21 +2274,6 @@ Qed.
 
 (** Unsigned right shifts and unsigned divisions by powers of 2. *)
 
-Lemma Zshiftr_div_two_p:
-  forall x n, 0 <= n -> Z.shiftr x n = x / two_p n.
-Proof.
-  intros. destruct n; unfold Z.shiftr; simpl.
-  - rewrite Zdiv_1_r. auto.
-  - pattern p. apply Pos.peano_ind.
-    + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div.
-    + intros. rewrite Pos.iter_succ. rewrite H0.
-      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
-      change (two_power_pos 1) with 2.
-      rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv.
-      rewrite two_power_pos_nat. apply two_power_nat_pos. omega.
-  - compute in H. congruence.
-Qed.
-
 Lemma shru_div_two_p:
   forall x y,
   shru x y = repr (unsigned x / two_p (unsigned y)).
@@ -2897,43 +2316,6 @@ Qed.
 
 (** Unsigned modulus over [2^n] is masking with [2^n-1]. *)
 
-Lemma Ztestbit_mod_two_p:
-  forall n x i,
-  0 <= n -> 0 <= i ->
-  Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false.
-Proof.
-  intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto.
-  - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l.
-    rewrite zlt_false; auto. omega.
-  - intros. rewrite two_p_S; auto.
-    replace (x0 mod (2 * two_p x))
-       with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)).
-    rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0).
-    + rewrite zlt_true; auto. omega.
-    + rewrite H0. destruct (zlt (Z.pred i) x).
-      * rewrite zlt_true; auto. omega.
-      * rewrite zlt_false; auto. omega.
-      * omega.
-    + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry.
-      apply Zmod_unique with (x1 / two_p x).
-      rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal.
-      transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)).
-      f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto.
-      ring.
-      rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto.
-      destruct (Z.odd x0); omega.
-Qed.
-
-Corollary Ztestbit_two_p_m1:
-  forall n i, 0 <= n -> 0 <= i ->
-  Z.testbit (two_p n - 1) i = if zlt i n then true else false.
-Proof.
-  intros. replace (two_p n - 1) with ((-1) mod (two_p n)).
-  rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto.
-  apply Zmod_unique with (-1). ring.
-  exploit (two_p_gt_ZERO n). auto. omega.
-Qed.
-
 Theorem modu_and:
   forall x n logn,
   is_power2 n = Some logn ->
@@ -2955,21 +2337,6 @@ Qed.
 
 (** ** Properties of [shrx] (signed division by a power of 2) *)
 
-Lemma Zquot_Zdiv:
-  forall x y,
-  y > 0 ->
-  Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.
-Proof.
-  intros. destruct (zlt x 0).
-  - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)).
-     + red. right; split. omega.
-       exploit (Z_mod_lt (x + y - 1) y); auto.
-       rewrite Z.abs_eq. omega. omega.
-     + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)).
-       rewrite <- Z_div_mod_eq. ring. auto. ring.
-  - apply Zquot_Zdiv_pos; omega.
-Qed.
-
 Theorem shrx_zero:
   forall x, zwordsize > 1 -> shrx x zero = x.
 Proof.
@@ -3048,17 +2415,6 @@ Proof.
   bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto.
 Qed.
 
-Lemma Zdiv_shift:
-  forall x y, y > 0 ->
-  (x + (y - 1)) / y = x / y + if zeq (Z.modulo x y) 0 then 0 else 1.
-Proof.
-  intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H).
-  set (q := x / y). set (r := x mod y). intros.
-  destruct (zeq r 0).
-  apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega.
-  apply Zdiv_unique with (r - 1). rewrite H1. ring. omega.
-Qed.
-
 Theorem shrx_carry:
   forall x y,
   ltu y (repr (zwordsize - 1)) = true ->
@@ -3149,51 +2505,6 @@ Qed.
 
 (** ** Properties of integer zero extension and sign extension. *)
 
-Lemma Ziter_base:
-  forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x.
-Proof.
-  intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto.
-Qed.
-
-Lemma Ziter_succ:
-  forall (A: Type) n (f: A -> A) x,
-  0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x).
-Proof.
-  intros. destruct n; simpl.
-  - auto.
-  - rewrite Pos.add_1_r. apply Pos.iter_succ.
-  - compute in H. elim H; auto.
-Qed.
-
-Lemma Znatlike_ind:
-  forall (P: Z -> Prop),
-  (forall n, n <= 0 -> P n) ->
-  (forall n, 0 <= n -> P n -> P (Z.succ n)) ->
-  forall n, P n.
-Proof.
-  intros. destruct (zle 0 n).
-  apply natlike_ind; auto. apply H; omega.
-  apply H. omega.
-Qed.
-
-Lemma Zzero_ext_spec:
-  forall n x i, 0 <= i ->
-  Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false.
-Proof.
-  unfold Zzero_ext. induction n using Znatlike_ind.
-  - intros. rewrite Ziter_base; auto.
-    rewrite zlt_false. rewrite Ztestbit_0; auto. omega.
-  - intros. rewrite Ziter_succ; auto.
-    rewrite Ztestbit_shiftin; auto.
-    rewrite (Ztestbit_eq i x); auto.
-    destruct (zeq i 0).
-    + subst i. rewrite zlt_true; auto. omega.
-    + rewrite IHn. destruct (zlt (Z.pred i) n).
-      rewrite zlt_true; auto. omega.
-      rewrite zlt_false; auto. omega.
-      omega.
-Qed.
-
 Lemma bits_zero_ext:
   forall n x i, 0 <= i ->
   testbit (zero_ext n x) i = if zlt i n then testbit x i else false.
@@ -3203,35 +2514,6 @@ Proof.
   rewrite !bits_above; auto. destruct (zlt i n); auto.
 Qed.
 
-Lemma Zsign_ext_spec:
-  forall n x i, 0 <= i -> 0 < n ->
-  Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1).
-Proof.
-  intros n0 x i I0 N0.
-  revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1).
-  - unfold Zsign_ext. intros.
-    destruct (zeq x 1).
-    + subst x; simpl.
-      replace (if zlt i 1 then i else 0) with 0.
-      rewrite Ztestbit_base.
-      destruct (Z.odd x0).
-      apply Ztestbit_m1; auto.
-      apply Ztestbit_0.
-      destruct (zlt i 1); omega.
-    + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)).
-      rewrite Ziter_succ. rewrite Ztestbit_shiftin.
-      destruct (zeq i 0).
-      * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega.
-      * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)).
-        rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega.
-        rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto.
-        omega. omega. omega. unfold x1; omega. omega.
-      * omega.
-      * unfold x1; omega.
-      * omega.
-  - omega.
-Qed.
-
 Lemma bits_sign_ext:
   forall n x i, 0 <= i < zwordsize -> 0 < n ->
   testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1).
@@ -3533,7 +2815,7 @@ Proof.
   auto with ints. decEq. apply Z_one_bits_powerserie.
   auto with ints.
   unfold one_bits.
-  generalize (Z_one_bits_range (unsigned x)).
+  generalize (Z_one_bits_range wordsize (unsigned x)).
   generalize (Z_one_bits wordsize (unsigned x) 0).
   induction l.
   intros; reflexivity.
@@ -3541,7 +2823,8 @@ Proof.
   apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut.
   rewrite mul_one. apply eqm_unsigned_repr_r.
   rewrite unsigned_repr. auto with ints.
-  generalize (H a (in_eq _ _)). generalize wordsize_max_unsigned. omega.
+  generalize (H a (in_eq _ _)). change (Z.of_nat wordsize) with zwordsize.
+  generalize wordsize_max_unsigned. omega.
   auto with ints.
   intros; apply H; auto with coqlib.
 Qed.
@@ -3741,8 +3024,7 @@ Proof.
   intros. rewrite <- negb_orb. rewrite <- not_ltu. rewrite negb_involutive. auto.
 Qed.
 
-
-(** Non-overlapping test *)
+(** ** Non-overlapping test *)
 
 Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=
   let x1 := unsigned ofs1 in let x2 := unsigned ofs2 in
@@ -3768,94 +3050,10 @@ Proof.
   intros [C|C] [D|D]; omega.
 Qed.
 
-(** Size of integers, in bits. *)
-
-Definition Zsize (x: Z) : Z :=
-  match x with
-  | Zpos p => Zpos (Pos.size p)
-  | _ => 0
-  end.
+(** ** Size of integers, in bits. *)
 
 Definition size (x: int) : Z := Zsize (unsigned x).
 
-Remark Zsize_pos: forall x, 0 <= Zsize x.
-Proof.
-  destruct x; simpl. omega. compute; intuition congruence. omega.
-Qed.
-
-Remark Zsize_pos': forall x, 0 < x -> 0 < Zsize x.
-Proof.
-  destruct x; simpl; intros; try discriminate. compute; auto.
-Qed.
-
-Lemma Zsize_shiftin:
-  forall b x, 0 < x -> Zsize (Zshiftin b x) = Z.succ (Zsize x).
-Proof.
-  intros. destruct x; compute in H; try discriminate.
-  destruct b.
-  change (Zshiftin true (Zpos p)) with (Zpos (p~1)).
-  simpl. f_equal. rewrite Pos.add_1_r; auto.
-  change (Zshiftin false (Zpos p)) with (Zpos (p~0)).
-  simpl. f_equal. rewrite Pos.add_1_r; auto.
-Qed.
-
-Lemma Ztestbit_size_1:
-  forall x, 0 < x -> Z.testbit x (Z.pred (Zsize x)) = true.
-Proof.
-  intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto.
-  intros. rewrite Zsize_shiftin; auto.
-  replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega.
-  rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega.
-Qed.
-
-Lemma Ztestbit_size_2:
-  forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false.
-Proof.
-  intros x0 POS0. destruct (zeq x0 0).
-  - subst x0; intros. apply Ztestbit_0.
-  - pattern x0; apply Zshiftin_pos_ind.
-    + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin.
-      rewrite zeq_false. apply Ztestbit_0. omega. omega.
-    + intros. rewrite Zsize_shiftin in H1; auto.
-      generalize (Zsize_pos' _ H); intros.
-      rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega.
-      omega. omega.
-    + omega.
-Qed.
-
-Lemma Zsize_interval_1:
-  forall x, 0 <= x -> 0 <= x < two_p (Zsize x).
-Proof.
-  intros.
-  assert (x = x mod (two_p (Zsize x))).
-    apply equal_same_bits; intros.
-    rewrite Ztestbit_mod_two_p; auto.
-    destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto.
-    apply Zsize_pos; auto.
-  rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto.
-Qed.
-
-Lemma Zsize_interval_2:
-  forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x.
-Proof.
-  intros. set (N := Z.to_nat n).
-  assert (Z.of_nat N = n) by (apply Z2Nat.id; auto).
-  rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0.
-  destruct (zeq x 0).
-  subst x; simpl; omega.
-  destruct (zlt n (Zsize x)); auto.
-  exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega.
-  rewrite Ztestbit_size_1. congruence. omega.
-Qed.
-
-Lemma Zsize_monotone:
-  forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
-Proof.
-  intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos.
-  exploit (Zsize_interval_1 y). omega.
-  omega.
-Qed.
-
 Theorem size_zero: size zero = 0.
 Proof.
   unfold size; rewrite unsigned_zero; auto.
@@ -4321,7 +3519,7 @@ Theorem one_bits'_range:
 Proof.
   intros.
   destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]].
-  exploit Z_one_bits_range; eauto. intros R.
+  exploit Z_one_bits_range; eauto. fold zwordsize. intros R.
   unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr.
   change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega.
   assert (zwordsize < Int.max_unsigned) by reflexivity. omega.
@@ -4380,7 +3578,7 @@ Lemma is_power2'_correct:
 Proof.
   unfold is_power2'; intros.
   destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv H.
-  rewrite (Z_one_bits_powerserie (unsigned n)) by (apply unsigned_range).
+  rewrite (Z_one_bits_powerserie wordsize (unsigned n)) by (apply unsigned_range).
   rewrite Int.unsigned_repr. rewrite B; simpl. omega.
   assert (0 <= i < zwordsize).
   { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. }
diff --git a/lib/Zbits.v b/lib/Zbits.v
new file mode 100644
index 00000000..74f66b6e
--- /dev/null
+++ b/lib/Zbits.v
@@ -0,0 +1,945 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Additional operations and proofs about binary integers,
+    on top of the ZArith standard library. *)
+
+Require Import Psatz Zquot.
+Require Import Coqlib.
+
+(** ** Modulo arithmetic *)
+
+(** We define and state properties of equality and arithmetic modulo a
+  positive integer. *)
+
+Section EQ_MODULO.
+
+Variable modul: Z.
+Hypothesis modul_pos: modul > 0.
+
+Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.
+
+Lemma eqmod_refl: forall x, eqmod x x.
+Proof.
+  intros; red. exists 0. omega.
+Qed.
+
+Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
+Proof.
+  intros. subst y. apply eqmod_refl.
+Qed.
+
+Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
+Proof.
+  intros x y [k EQ]; red. exists (-k). subst x. ring.
+Qed.
+
+Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
+Proof.
+  intros x y z [k1 EQ1] [k2 EQ2]; red.
+  exists (k1 + k2). subst x; subst y. ring.
+Qed.
+
+Lemma eqmod_small_eq:
+  forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
+Proof.
+  intros x y [k EQ] I1 I2.
+  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
+  rewrite (Z.div_small x modul I1) in H. subst k. omega.
+Qed.
+
+Lemma eqmod_mod_eq:
+  forall x y, eqmod x y -> x mod modul = y mod modul.
+Proof.
+  intros x y [k EQ]. subst x.
+  rewrite Z.add_comm. apply Z_mod_plus. auto.
+Qed.
+
+Lemma eqmod_mod:
+  forall x, eqmod x (x mod modul).
+Proof.
+  intros; red. exists (x / modul).
+  rewrite Z.mul_comm. apply Z_div_mod_eq. auto.
+Qed.
+
+Lemma eqmod_add:
+  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst c. exists (k1 + k2). ring.
+Qed.
+
+Lemma eqmod_neg:
+  forall x y, eqmod x y -> eqmod (-x) (-y).
+Proof.
+  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
+Qed.
+
+Lemma eqmod_sub:
+  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst c. exists (k1 - k2). ring.
+Qed.
+
+Lemma eqmod_mult:
+  forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst b.
+  exists (k1 * k2 * modul + c * k2 + k1 * d).
+  ring.
+Qed.
+
+End EQ_MODULO.
+
+Lemma eqmod_divides:
+  forall n m x y, eqmod n x y -> Z.divide m n -> eqmod m x y.
+Proof.
+  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
+  exists (k1*k2). rewrite <- Z.mul_assoc. rewrite <- EQ2. auto.
+Qed.
+
+(** ** Fast normalization modulo [2^n] *)
+
+Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z :=
+  match n with
+  | O => 0
+  | S m =>
+      match p with
+      | xH => 1
+      | xO q => Z.double (P_mod_two_p q m)
+      | xI q => Z.succ_double (P_mod_two_p q m)
+      end
+  end.
+
+Definition Z_mod_two_p (x: Z) (n: nat) : Z :=
+  match x with
+  | Z0 => 0
+  | Zpos p => P_mod_two_p p n
+  | Zneg p => let r := P_mod_two_p p n in if zeq r 0 then 0 else two_power_nat n - r
+  end.
+
+Lemma P_mod_two_p_range:
+  forall n p, 0 <= P_mod_two_p p n < two_power_nat n.
+Proof.
+  induction n; simpl; intros.
+  - rewrite two_power_nat_O. omega.
+  - rewrite two_power_nat_S. destruct p.
+    + generalize (IHn p). rewrite Z.succ_double_spec. omega.
+    + generalize (IHn p). rewrite Z.double_spec. omega.
+    + generalize (two_power_nat_pos n). omega.
+Qed.
+
+Lemma P_mod_two_p_eq:
+  forall n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).
+Proof.
+  assert (forall n p, exists y, Zpos p = y * two_power_nat n + P_mod_two_p p n).
+  {
+    induction n; simpl; intros.
+    - rewrite two_power_nat_O. exists (Zpos p). ring.
+    - rewrite two_power_nat_S. destruct p.
+      + destruct (IHn p) as [y EQ]. exists y.
+        change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ.
+        rewrite Z.succ_double_spec. ring.
+      + destruct (IHn p) as [y EQ]. exists y.
+        change (Zpos p~0) with (2 * Zpos p). rewrite EQ.
+        rewrite (Z.double_spec (P_mod_two_p p n)). ring.
+      + exists 0; omega.
+  }
+  intros.
+  destruct (H n p) as [y EQ].
+  symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range.
+Qed.
+
+Lemma Z_mod_two_p_range:
+  forall n x, 0 <= Z_mod_two_p x n < two_power_nat n.
+Proof.
+  intros; unfold Z_mod_two_p. generalize (two_power_nat_pos n); intros.
+  destruct x.
+  - intuition.
+  - apply P_mod_two_p_range.
+  - set (r := P_mod_two_p p n).
+    assert (0 <= r < two_power_nat n) by apply P_mod_two_p_range.
+    destruct (zeq r 0).
+    + intuition.
+    + Psatz.lia.
+Qed.
+
+Lemma Z_mod_two_p_eq:
+  forall n x, Z_mod_two_p x n = x mod (two_power_nat n).
+Proof.
+  intros. unfold Z_mod_two_p. generalize (two_power_nat_pos n); intros.
+  destruct x.
+  - rewrite Zmod_0_l. auto.
+  - apply P_mod_two_p_eq.
+  - generalize (P_mod_two_p_range n p) (P_mod_two_p_eq n p). intros A B.
+    exploit (Z_div_mod_eq (Zpos p) (two_power_nat n)); auto. intros C.
+    set (q := Zpos p / two_power_nat n) in *.
+    set (r := P_mod_two_p p n) in *.
+    rewrite <- B in C.
+    change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0).
+    + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia.
+      intuition.
+    + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia.
+      intuition.
+Qed.
+
+(** ** Bit-level operations and properties *)
+
+(** Shift [x] left by one and insert [b] as the low bit of the result. *)
+
+Definition Zshiftin (b: bool) (x: Z) : Z :=
+  if b then Z.succ_double x else Z.double x.
+
+Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
+Proof Z.testbit_0_l.
+
+Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
+Proof.
+  intros. destruct n; simpl; auto.
+Qed.
+
+Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
+Proof.
+  intros. destruct n; simpl; auto.
+Qed.
+
+Remark Zshiftin_spec:
+  forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0).
+Proof.
+  unfold Zshiftin; intros. destruct b.
+  - rewrite Z.succ_double_spec. omega.
+  - rewrite Z.double_spec. omega.
+Qed.
+
+Remark Zshiftin_inj:
+  forall b1 x1 b2 x2,
+  Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2.
+Proof.
+  intros. rewrite !Zshiftin_spec in H.
+  destruct b1; destruct b2.
+  split; [auto|omega].
+  omegaContradiction.
+  omegaContradiction.
+  split; [auto|omega].
+Qed.
+
+Remark Zdecomp:
+  forall x, x = Zshiftin (Z.odd x) (Z.div2 x).
+Proof.
+  intros. destruct x; simpl.
+  - auto.
+  - destruct p; auto.
+  - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto.
+Qed.
+
+Remark Ztestbit_shiftin:
+  forall b x n,
+  0 <= n ->
+  Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n).
+Proof.
+  intros. rewrite Zshiftin_spec. destruct (zeq n 0).
+  - subst n. destruct b.
+    + apply Z.testbit_odd_0.
+    + rewrite Z.add_0_r. apply Z.testbit_even_0.
+  - assert (0 <= Z.pred n) by omega.
+    set (n' := Z.pred n) in *.
+    replace n with (Z.succ n') by (unfold n'; omega).
+    destruct b.
+    + apply Z.testbit_odd_succ; auto.
+    + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto.
+Qed.
+
+Remark Ztestbit_shiftin_base:
+  forall b x, Z.testbit (Zshiftin b x) 0 = b.
+Proof.
+  intros. rewrite Ztestbit_shiftin. apply zeq_true. omega.
+Qed.
+
+Remark Ztestbit_shiftin_succ:
+  forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.
+Proof.
+  intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto.
+  omega. omega.
+Qed.
+
+Lemma Zshiftin_ind:
+  forall (P: Z -> Prop),
+  P 0 ->
+  (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) ->
+  forall x, 0 <= x -> P x.
+Proof.
+  intros. destruct x.
+  - auto.
+  - induction p.
+    + change (P (Zshiftin true (Z.pos p))). auto.
+    + change (P (Zshiftin false (Z.pos p))). auto.
+    + change (P (Zshiftin true 0)). apply H0. omega. auto.
+  - compute in H1. intuition congruence.
+Qed.
+
+Lemma Zshiftin_pos_ind:
+  forall (P: Z -> Prop),
+  P 1 ->
+  (forall b x, 0 < x -> P x -> P (Zshiftin b x)) ->
+  forall x, 0 < x -> P x.
+Proof.
+  intros. destruct x; simpl in H1; try discriminate.
+  induction p.
+    + change (P (Zshiftin true (Z.pos p))). auto.
+    + change (P (Zshiftin false (Z.pos p))). auto.
+    + auto.
+Qed.
+
+(** ** Bit-wise decomposition ([Z.testbit]) *)
+
+Remark Ztestbit_eq:
+  forall n x, 0 <= n ->
+  Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n).
+Proof.
+  intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto.
+Qed.
+
+Remark Ztestbit_base:
+  forall x, Z.testbit x 0 = Z.odd x.
+Proof.
+  intros. rewrite Ztestbit_eq. apply zeq_true. omega.
+Qed.
+
+Remark Ztestbit_succ:
+  forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.
+Proof.
+  intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto.
+  omega. omega.
+Qed.
+
+Lemma eqmod_same_bits:
+  forall n x y,
+  (forall i, 0 <= i < Z.of_nat n -> Z.testbit x i = Z.testbit y i) ->
+  eqmod (two_power_nat n) x y.
+Proof.
+  induction n; intros.
+  - change (two_power_nat 0) with 1. exists (x-y); ring.
+  - rewrite two_power_nat_S.
+    assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)).
+      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega.
+      omega. omega.
+  destruct H0 as [k EQ].
+  exists k. rewrite (Zdecomp x). rewrite (Zdecomp y).
+  replace (Z.odd y) with (Z.odd x).
+  rewrite EQ. rewrite !Zshiftin_spec. ring.
+  exploit (H 0). rewrite Nat2Z.inj_succ; omega.
+  rewrite !Ztestbit_base. auto.
+Qed.
+
+Lemma same_bits_eqmod:
+  forall n x y i,
+  eqmod (two_power_nat n) x y -> 0 <= i < Z.of_nat n ->
+  Z.testbit x i = Z.testbit y i.
+Proof.
+  induction n; intros.
+  - simpl in H0. omegaContradiction.
+  - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H.
+    rewrite !(Ztestbit_eq i); intuition.
+    destruct H as [k EQ].
+    assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) =
+                 Zshiftin (Z.odd y) (k * two_power_nat n + Z.div2 y)).
+    {
+      rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ.
+      rewrite EQ. rewrite !Zshiftin_spec. ring.
+    }
+    exploit Zshiftin_inj; eauto. intros [A B].
+    destruct (zeq i 0).
+    + auto.
+    + apply IHn. exists k; auto. omega.
+Qed.
+
+Lemma equal_same_bits:
+  forall x y,
+  (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
+  x = y.
+Proof Z.bits_inj'.
+
+Lemma Z_one_complement:
+  forall i, 0 <= i ->
+  forall x, Z.testbit (-x-1) i = negb (Z.testbit x i).
+Proof.
+  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
+  intros i IND POS x.
+  rewrite (Zdecomp x). set (y := Z.div2 x).
+  replace (- Zshiftin (Z.odd x) y - 1)
+     with (Zshiftin (negb (Z.odd x)) (- y - 1)).
+  rewrite !Ztestbit_shiftin; auto.
+  destruct (zeq i 0). auto. apply IND. omega.
+  rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring.
+Qed.
+
+Lemma Ztestbit_above:
+  forall n x i,
+  0 <= x < two_power_nat n ->
+  i >= Z.of_nat n ->
+  Z.testbit x i = false.
+Proof.
+  induction n; intros.
+  - change (two_power_nat 0) with 1 in H.
+    replace x with 0 by omega.
+    apply Z.testbit_0_l.
+  - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false.
+    apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H.
+    rewrite Zshiftin_spec in H. destruct (Z.odd x); omega.
+    omega. omega. omega.
+Qed.
+
+Lemma Ztestbit_above_neg:
+  forall n x i,
+  -two_power_nat n <= x < 0 ->
+  i >= Z.of_nat n ->
+  Z.testbit x i = true.
+Proof.
+  intros. set (y := -x-1).
+  assert (Z.testbit y i = false).
+    apply Ztestbit_above with n.
+    unfold y; omega. auto.
+  unfold y in H1. rewrite Z_one_complement in H1.
+  change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto.
+  omega.
+Qed.
+
+Lemma Zsign_bit:
+  forall n x,
+  0 <= x < two_power_nat (S n) ->
+  Z.testbit x (Z.of_nat n) = if zlt x (two_power_nat n) then false else true.
+Proof.
+  induction n; intros.
+  - change (two_power_nat 1) with 2 in H.
+    assert (x = 0 \/ x = 1) by omega.
+    destruct H0; subst x; reflexivity.
+  - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
+    rewrite IHn. rewrite two_power_nat_S.
+    destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec.
+    rewrite zlt_true. auto. destruct (Z.odd x); omega.
+    rewrite zlt_false. auto. destruct (Z.odd x); omega.
+    rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H.
+    rewrite two_power_nat_S in H. destruct (Z.odd x); omega.
+    omega. omega.
+Qed.
+
+Lemma Ztestbit_le:
+  forall x y,
+  0 <= y ->
+  (forall i, 0 <= i -> Z.testbit x i = true -> Z.testbit y i = true) ->
+  x <= y.
+Proof.
+  intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros.
+  - replace x with 0. omega. apply equal_same_bits; intros.
+    rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto.
+    exploit H; eauto. rewrite Ztestbit_0. auto.
+  - assert (Z.div2 x0 <= x).
+    { apply H0. intros. exploit (H1 (Z.succ i)).
+        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
+    }
+    rewrite (Zdecomp x0). rewrite !Zshiftin_spec.
+    destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega.
+    exploit (H1 0). omega. rewrite Ztestbit_base; auto.
+    rewrite Ztestbit_shiftin_base. congruence.
+Qed.
+
+Lemma Ztestbit_mod_two_p:
+  forall n x i,
+  0 <= n -> 0 <= i ->
+  Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false.
+Proof.
+  intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto.
+  - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l.
+    rewrite zlt_false; auto. omega.
+  - intros. rewrite two_p_S; auto.
+    replace (x0 mod (2 * two_p x))
+       with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)).
+    rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0).
+    + rewrite zlt_true; auto. omega.
+    + rewrite H0. destruct (zlt (Z.pred i) x).
+      * rewrite zlt_true; auto. omega.
+      * rewrite zlt_false; auto. omega.
+      * omega.
+    + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry.
+      apply Zmod_unique with (x1 / two_p x).
+      rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal.
+      transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)).
+      f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto.
+      ring.
+      rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto.
+      destruct (Z.odd x0); omega.
+Qed.
+
+Corollary Ztestbit_two_p_m1:
+  forall n i, 0 <= n -> 0 <= i ->
+  Z.testbit (two_p n - 1) i = if zlt i n then true else false.
+Proof.
+  intros. replace (two_p n - 1) with ((-1) mod (two_p n)).
+  rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto.
+  apply Zmod_unique with (-1). ring.
+  exploit (two_p_gt_ZERO n). auto. omega.
+Qed.
+
+Corollary Ztestbit_neg_two_p:
+  forall n i, 0 <= n -> 0 <= i ->
+  Z.testbit (- (two_p n)) i = if zlt i n then false else true.
+Proof.
+  intros. 
+  replace (- two_p n) with (- (two_p n - 1) - 1) by omega. 
+  rewrite Z_one_complement by auto.
+  rewrite Ztestbit_two_p_m1 by auto. 
+  destruct (zlt i n); auto.
+Qed.
+
+Lemma Z_add_is_or:
+  forall i, 0 <= i ->
+  forall x y,
+  (forall j, 0 <= j <= i -> Z.testbit x j && Z.testbit y j = false) ->
+  Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.
+Proof.
+  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
+  intros i IND POS x y EXCL.
+  rewrite (Zdecomp x) in *. rewrite (Zdecomp y) in *.
+  transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i).
+  - f_equal. rewrite !Zshiftin_spec.
+    exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros.
+Opaque Z.mul.
+    destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring.
+  - rewrite !Ztestbit_shiftin; auto.
+    destruct (zeq i 0).
+    + auto.
+    + apply IND. omega. intros.
+      exploit (EXCL (Z.succ j)). omega.
+      rewrite !Ztestbit_shiftin_succ. auto.
+      omega. omega.
+Qed.
+
+(** ** Zero and sign extensions *)
+
+(** In pseudo-code:
+<<
+    Fixpoint Zzero_ext (n: Z) (x: Z) : Z :=
+      if zle n 0 then
+        0
+      else
+        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
+    Fixpoint Zsign_ext (n: Z) (x: Z) : Z :=
+      if zle n 1 then
+        if Z.odd x then -1 else 0
+      else
+        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
+>>
+  We encode this [nat]-like recursion using the [Z.iter] iteration
+  function, in order to make the [Zzero_ext] and [Zsign_ext]
+  functions efficiently executable within Coq.
+*)
+
+Definition Zzero_ext (n: Z) (x: Z) : Z :=
+  Z.iter n
+    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
+    (fun x => 0)
+    x.
+
+Definition Zsign_ext (n: Z) (x: Z) : Z :=
+  Z.iter (Z.pred n)
+    (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
+    (fun x => if Z.odd x then -1 else 0)
+    x.
+
+Lemma Ziter_base:
+  forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x.
+Proof.
+  intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto.
+Qed.
+
+Lemma Ziter_succ:
+  forall (A: Type) n (f: A -> A) x,
+  0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x).
+Proof.
+  intros. destruct n; simpl.
+  - auto.
+  - rewrite Pos.add_1_r. apply Pos.iter_succ.
+  - compute in H. elim H; auto.
+Qed.
+
+Lemma Znatlike_ind:
+  forall (P: Z -> Prop),
+  (forall n, n <= 0 -> P n) ->
+  (forall n, 0 <= n -> P n -> P (Z.succ n)) ->
+  forall n, P n.
+Proof.
+  intros. destruct (zle 0 n).
+  apply natlike_ind; auto. apply H; omega.
+  apply H. omega.
+Qed.
+
+Lemma Zzero_ext_spec:
+  forall n x i, 0 <= i ->
+  Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false.
+Proof.
+  unfold Zzero_ext. induction n using Znatlike_ind.
+  - intros. rewrite Ziter_base; auto.
+    rewrite zlt_false. rewrite Ztestbit_0; auto. omega.
+  - intros. rewrite Ziter_succ; auto.
+    rewrite Ztestbit_shiftin; auto.
+    rewrite (Ztestbit_eq i x); auto.
+    destruct (zeq i 0).
+    + subst i. rewrite zlt_true; auto. omega.
+    + rewrite IHn. destruct (zlt (Z.pred i) n).
+      rewrite zlt_true; auto. omega.
+      rewrite zlt_false; auto. omega.
+      omega.
+Qed.
+
+Lemma Zsign_ext_spec:
+  forall n x i, 0 <= i -> 0 < n ->
+  Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1).
+Proof.
+  intros n0 x i I0 N0.
+  revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1).
+  - unfold Zsign_ext. intros.
+    destruct (zeq x 1).
+    + subst x; simpl.
+      replace (if zlt i 1 then i else 0) with 0.
+      rewrite Ztestbit_base.
+      destruct (Z.odd x0).
+      apply Ztestbit_m1; auto.
+      apply Ztestbit_0.
+      destruct (zlt i 1); omega.
+    + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)).
+      rewrite Ziter_succ. rewrite Ztestbit_shiftin.
+      destruct (zeq i 0).
+      * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega.
+      * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)).
+        rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega.
+        rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto.
+        omega. omega. omega. unfold x1; omega. omega.
+      * omega.
+      * unfold x1; omega.
+      * omega.
+  - omega.
+Qed.
+
+(** [Zzero_ext n x] is [x modulo 2^n] *)
+
+Lemma Zzero_ext_mod:
+  forall n x, 0 <= n -> Zzero_ext n x = x mod (two_p n).
+Proof.
+  intros. apply equal_same_bits; intros.
+  rewrite Zzero_ext_spec, Ztestbit_mod_two_p by auto. auto.
+Qed.
+
+(** [Zzero_ext n x] is the unique integer congruent to [x] modulo [2^n] in the range [0...2^n-1]. *)
+
+Lemma Zzero_ext_range:
+  forall n x, 0 <= n -> 0 <= Zzero_ext n x < two_p n.
+Proof.
+  intros. rewrite Zzero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega.
+Qed.
+
+Lemma eqmod_Zzero_ext:
+  forall n x, 0 <= n -> eqmod (two_p n) (Zzero_ext n x) x.
+Proof.
+  intros. rewrite Zzero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod.
+  apply two_p_gt_ZERO. omega.
+Qed.
+
+(** Relation between [Zsign_ext n x] and (Zzero_ext n x] *)
+
+Lemma Zsign_ext_zero_ext:
+  forall n, 0 < n -> forall x,
+  Zsign_ext n x = Zzero_ext n x - (if Z.testbit x (n - 1) then two_p n else 0).
+Proof.
+  intros. apply equal_same_bits; intros.
+  rewrite Zsign_ext_spec by auto.
+  destruct (Z.testbit x (n - 1)) eqn:SIGNBIT.
+- set (n' := - two_p n). 
+  replace (Zzero_ext n x - two_p n) with (Zzero_ext n x + n') by (unfold n'; omega).
+  rewrite Z_add_is_or; auto. 
+  rewrite Zzero_ext_spec by auto. unfold n'; rewrite Ztestbit_neg_two_p by omega.
+  destruct (zlt i n). rewrite orb_false_r; auto. auto.
+  intros. rewrite Zzero_ext_spec by omega. unfold n'; rewrite Ztestbit_neg_two_p by omega.
+  destruct (zlt j n); auto using andb_false_r.
+- replace (Zzero_ext n x - 0) with (Zzero_ext n x) by omega.
+  rewrite Zzero_ext_spec by auto.
+  destruct (zlt i n); auto.
+Qed.
+
+(** [Zsign_ext n x] is the unique integer congruent to [x] modulo [2^n]
+    in the range [-2^(n-1)...2^(n-1) - 1]. *)
+
+Lemma Zsign_ext_range:
+  forall n x, 0 < n -> -two_p (n-1) <= Zsign_ext n x < two_p (n-1).
+Proof.
+  intros.
+  assert (A: 0 <= Zzero_ext n x < two_p n) by (apply Zzero_ext_range; omega).
+  assert (B: Z.testbit (Zzero_ext n x) (n - 1) =
+             if zlt (Zzero_ext n x) (two_p (n - 1)) then false else true).
+  { set (N := Z.to_nat (n - 1)).
+    generalize (Zsign_bit N (Zzero_ext n x)). 
+    rewrite ! two_power_nat_two_p.
+    rewrite inj_S.  unfold N; rewrite Z2Nat.id by omega.
+    intros X; apply X.  replace (Z.succ (n - 1)) with n by omega. exact A. 
+  }
+  assert (C: two_p n = 2 * two_p (n - 1)).
+  { rewrite <- two_p_S by omega. f_equal; omega. }
+  rewrite Zzero_ext_spec, zlt_true in B by omega.
+  rewrite Zsign_ext_zero_ext by auto. rewrite B.
+  destruct (zlt (Zzero_ext n x) (two_p (n - 1))); omega.
+Qed.
+
+Lemma eqmod_Zsign_ext:
+  forall n x, 0 < n ->
+  eqmod (two_p n) (Zsign_ext n x) x.
+Proof.
+  intros. rewrite Zsign_ext_zero_ext by auto. 
+  apply eqmod_trans with (x - 0). 
+  apply eqmod_sub. 
+  apply eqmod_Zzero_ext; omega.
+  exists (if Z.testbit x (n - 1) then 1 else 0). destruct (Z.testbit x (n - 1)); ring.
+  apply eqmod_refl2; omega.
+Qed.
+
+(** ** Decomposition of a number as a sum of powers of two. *)
+
+Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
+  match n with
+  | O => nil
+  | S m =>
+      if Z.odd x
+      then i :: Z_one_bits m (Z.div2 x) (i+1)
+      else Z_one_bits m (Z.div2 x) (i+1)
+  end.
+
+Fixpoint powerserie (l: list Z): Z :=
+  match l with
+  | nil => 0
+  | x :: xs => two_p x + powerserie xs
+  end.
+
+Lemma Z_one_bits_powerserie:
+  forall n x, 0 <= x < two_power_nat n -> x = powerserie (Z_one_bits n x 0).
+Proof.
+  assert (forall n x i,
+    0 <= i ->
+    0 <= x < two_power_nat n ->
+    x * two_p i = powerserie (Z_one_bits n x i)).
+  {
+  induction n; intros.
+  simpl. rewrite two_power_nat_O in H0.
+  assert (x = 0) by omega. subst x. omega.
+  rewrite two_power_nat_S in H0. simpl Z_one_bits.
+  rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0.
+  assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))).
+    apply IHn. omega.
+    destruct (Z.odd x); omega.
+  rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ.
+  rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec.
+  destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring.
+  omega. omega.
+  }
+  intros. rewrite <- H. change (two_p 0) with 1. omega.
+  omega. exact H0.
+Qed.
+
+Lemma Z_one_bits_range:
+  forall n x i, In i (Z_one_bits n x 0) -> 0 <= i < Z.of_nat n.
+Proof.
+  assert (forall n x i j,
+    In j (Z_one_bits n x i) -> i <= j < i + Z.of_nat n).
+  {
+  induction n; simpl In.
+  tauto.
+  intros x i j. rewrite Nat2Z.inj_succ.
+  assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)).
+    intros. exploit IHn; eauto. omega.
+  destruct (Z.odd x); simpl.
+  intros [A|B]. subst j. omega. auto.
+  auto.
+  }
+  intros. generalize (H n x 0 i H0). omega.
+Qed.
+
+Remark Z_one_bits_zero:
+  forall n i, Z_one_bits n 0 i = nil.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.
+
+Remark Z_one_bits_two_p:
+  forall n x i,
+  0 <= x < Z.of_nat n ->
+  Z_one_bits n (two_p x) i = (i + x) :: nil.
+Proof.
+  induction n; intros; simpl. simpl in H. omegaContradiction.
+  rewrite Nat2Z.inj_succ in H.
+  assert (x = 0 \/ 0 < x) by omega. destruct H0.
+  subst x; simpl. decEq. omega. apply Z_one_bits_zero.
+  assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)).
+    apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec.
+    rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega.
+  destruct H1 as [A B]; rewrite A; rewrite B.
+  rewrite IHn. f_equal; omega. omega.
+Qed.
+
+(** ** Relation between bitwise operations and multiplications / divisions by powers of 2 *)
+
+(** Left shifts and multiplications by powers of 2. *)
+
+Lemma Zshiftl_mul_two_p:
+  forall x n, 0 <= n -> Z.shiftl x n = x * two_p n.
+Proof.
+  intros. destruct n; simpl.
+  - omega.
+  - pattern p. apply Pos.peano_ind.
+    + change (two_power_pos 1) with 2. simpl. ring.
+    + intros. rewrite Pos.iter_succ. rewrite H0.
+      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
+      change (two_power_pos 1) with 2. ring.
+  - compute in H. congruence.
+Qed.
+
+(** Right shifts and divisions by powers of 2. *)
+
+Lemma Zshiftr_div_two_p:
+  forall x n, 0 <= n -> Z.shiftr x n = x / two_p n.
+Proof.
+  intros. destruct n; unfold Z.shiftr; simpl.
+  - rewrite Zdiv_1_r. auto.
+  - pattern p. apply Pos.peano_ind.
+    + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div.
+    + intros. rewrite Pos.iter_succ. rewrite H0.
+      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
+      change (two_power_pos 1) with 2.
+      rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv.
+      rewrite two_power_pos_nat. apply two_power_nat_pos. omega.
+  - compute in H. congruence.
+Qed.
+
+(** ** Properties of [shrx] (signed division by a power of 2) *)
+
+Lemma Zquot_Zdiv:
+  forall x y,
+  y > 0 ->
+  Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.
+Proof.
+  intros. destruct (zlt x 0).
+  - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)).
+     + red. right; split. omega.
+       exploit (Z_mod_lt (x + y - 1) y); auto.
+       rewrite Z.abs_eq. omega. omega.
+     + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)).
+       rewrite <- Z_div_mod_eq. ring. auto. ring.
+  - apply Zquot_Zdiv_pos; omega.
+Qed.
+
+Lemma Zdiv_shift:
+  forall x y, y > 0 ->
+  (x + (y - 1)) / y = x / y + if zeq (Z.modulo x y) 0 then 0 else 1.
+Proof.
+  intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H).
+  set (q := x / y). set (r := x mod y). intros.
+  destruct (zeq r 0).
+  apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega.
+  apply Zdiv_unique with (r - 1). rewrite H1. ring. omega.
+Qed.
+
+(** ** Size of integers, in bits. *)
+
+Definition Zsize (x: Z) : Z :=
+  match x with
+  | Zpos p => Zpos (Pos.size p)
+  | _ => 0
+  end.
+
+Remark Zsize_pos: forall x, 0 <= Zsize x.
+Proof.
+  destruct x; simpl. omega. compute; intuition congruence. omega.
+Qed.
+
+Remark Zsize_pos': forall x, 0 < x -> 0 < Zsize x.
+Proof.
+  destruct x; simpl; intros; try discriminate. compute; auto.
+Qed.
+
+Lemma Zsize_shiftin:
+  forall b x, 0 < x -> Zsize (Zshiftin b x) = Z.succ (Zsize x).
+Proof.
+  intros. destruct x; compute in H; try discriminate.
+  destruct b.
+  change (Zshiftin true (Zpos p)) with (Zpos (p~1)).
+  simpl. f_equal. rewrite Pos.add_1_r; auto.
+  change (Zshiftin false (Zpos p)) with (Zpos (p~0)).
+  simpl. f_equal. rewrite Pos.add_1_r; auto.
+Qed.
+
+Lemma Ztestbit_size_1:
+  forall x, 0 < x -> Z.testbit x (Z.pred (Zsize x)) = true.
+Proof.
+  intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto.
+  intros. rewrite Zsize_shiftin; auto.
+  replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega.
+  rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega.
+Qed.
+
+Lemma Ztestbit_size_2:
+  forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false.
+Proof.
+  intros x0 POS0. destruct (zeq x0 0).
+  - subst x0; intros. apply Ztestbit_0.
+  - pattern x0; apply Zshiftin_pos_ind.
+    + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin.
+      rewrite zeq_false. apply Ztestbit_0. omega. omega.
+    + intros. rewrite Zsize_shiftin in H1; auto.
+      generalize (Zsize_pos' _ H); intros.
+      rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega.
+      omega. omega.
+    + omega.
+Qed.
+
+Lemma Zsize_interval_1:
+  forall x, 0 <= x -> 0 <= x < two_p (Zsize x).
+Proof.
+  intros.
+  assert (x = x mod (two_p (Zsize x))).
+    apply equal_same_bits; intros.
+    rewrite Ztestbit_mod_two_p; auto.
+    destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto.
+    apply Zsize_pos; auto.
+  rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto.
+Qed.
+
+Lemma Zsize_interval_2:
+  forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x.
+Proof.
+  intros. set (N := Z.to_nat n).
+  assert (Z.of_nat N = n) by (apply Z2Nat.id; auto).
+  rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0.
+  destruct (zeq x 0).
+  subst x; simpl; omega.
+  destruct (zlt n (Zsize x)); auto.
+  exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega.
+  rewrite Ztestbit_size_1. congruence. omega.
+Qed.
+
+Lemma Zsize_monotone:
+  forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
+Proof.
+  intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos.
+  exploit (Zsize_interval_1 y). omega.
+  omega.
+Qed.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index c18757b2..afbba882 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -80,13 +81,13 @@ Proof.
     unfold Int.modu, Int.zero. decEq.
     change 0 with (0 mod 65536).
     change (Int.unsigned (Int.repr 65536)) with 65536.
-    apply Int.eqmod_mod_eq. omega.
-    unfold x, low_s. eapply Int.eqmod_trans.
-    apply Int.eqmod_divides with Int.modulus.
+    apply eqmod_mod_eq. omega.
+    unfold x, low_s. eapply eqmod_trans.
+    apply  eqmod_divides with Int.modulus.
     unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
     exists 65536. compute; auto.
     replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'.
+    apply eqmod_sub. apply eqmod_refl. apply Int.eqmod_sign_ext'.
     compute; auto.
   rewrite H0 in H. rewrite Int.add_zero in H.
   rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc.
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index a214d131..f16c967e 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Integers Floats Errors.
+Require Import String Coqlib Maps Zbits Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
@@ -221,11 +221,11 @@ Proof.
   change (Int64.unsigned Int64.iwordsize) with 64.
   f_equal.
   rewrite Int.unsigned_repr. 
-  apply Int.eqmod_mod_eq. omega. 
-  apply Int.eqmod_trans with a.
-  apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
+  apply eqmod_mod_eq. omega. 
+  apply eqmod_trans with a.
+  apply eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
   exists (two_p (32-6)); auto.
-  apply Int.eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr.
+  apply eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr.
   exists (two_p (64-6)); auto.
   assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega).
   assert (64 < Int.max_unsigned) by (compute; auto).
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 7f070c12..98d5bd33 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -16,7 +16,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib Errors Maps.
-Require Import AST Integers Floats Values Memory Globalenvs.
+Require Import AST Zbits Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Mach Conventions.
 Require Import Asm Asmgen Asmgenproof0.
 
@@ -33,16 +33,16 @@ Proof.
   predSpec Int.eq Int.eq_spec n lo.
 - auto.
 - set (m := Int.sub n lo).
-  assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
-  assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
+  assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
+  assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
   { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    auto using Int.eqmod_sub, Int.eqmod_refl. }
-  assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0).
-  { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
-    apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+    auto using eqmod_sub, eqmod_refl. }
+  assert (C: eqmod (two_p 12) (Int.unsigned m) 0).
+  { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
+    apply eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
     exists (two_p (32-12)); auto. }
   assert (D: Int.modu m (Int.repr 4096) = Int.zero).
-  { apply Int.eqmod_mod_eq in C. unfold Int.modu. 
+  { apply eqmod_mod_eq in C. unfold Int.modu. 
     change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
     reflexivity.
     apply two_p_gt_ZERO; omega. }
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 90f077db..d12bd8af 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -20,6 +20,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -372,7 +373,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.
@@ -400,7 +401,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.