Updated PR by removing whitespaces. Bug 17450.

1 files changed, 618 insertions, 618 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index a3ff5209..a0140e57 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -133,16 +133,16 @@ Proof.
     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. 
+      + 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]. 
+  intros.
+  destruct (H n p) as [y EQ].
   symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range.
 Qed.
 
@@ -150,12 +150,12 @@ Lemma Z_mod_modulus_range:
   forall x, 0 <= Z_mod_modulus x < modulus.
 Proof.
   intros; unfold Z_mod_modulus.
-  destruct x. 
+  destruct x.
   - generalize modulus_pos; omega.
   - 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). 
+    destruct (zeq r 0).
     + generalize modulus_pos; omega.
     + omega.
 Qed.
@@ -171,22 +171,22 @@ Lemma Z_mod_modulus_eq:
 Proof.
   intros. unfold Z_mod_modulus. destruct x.
   - rewrite Zmod_0_l. auto.
-  - apply P_mod_two_p_eq. 
+  - 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. 
+    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. ring.  
+    + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring.
       generalize modulus_pos; omega.
     + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring.
       omega.
 Qed.
 
 (** The [unsigned] and [signed] functions return the Coq integer corresponding
-  to the given machine integer, interpreted as unsigned or signed 
+  to the given machine integer, interpreted as unsigned or signed
   respectively. *)
 
 Definition unsigned (n: int) : Z := intval n.
@@ -198,7 +198,7 @@ Definition signed (n: int) : Z :=
 (** Conversely, [repr] takes a Coq integer and returns the corresponding
   machine integer.  The argument is treated modulo [modulus]. *)
 
-Definition repr (x: Z) : int := 
+Definition repr (x: Z) : int :=
   mkint (Z_mod_modulus x) (Z_mod_modulus_range' x).
 
 Definition zero := repr 0.
@@ -212,12 +212,12 @@ Proof.
   intros. subst y.
   assert (forall (n m: Z) (P1 P2: n < m), P1 = P2).
   {
-    unfold Zlt; intros. 
-    apply eq_proofs_unicity. 
+    unfold Zlt; intros.
+    apply eq_proofs_unicity.
     intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence).
   }
   destruct Px as [Px1 Px2]. destruct Py as [Py1 Py2].
-  rewrite (H _ _ Px1 Py1). 
+  rewrite (H _ _ Px1 Py1).
   rewrite (H _ _ Px2 Py2).
   reflexivity.
 Qed.
@@ -231,7 +231,7 @@ Defined.
 
 (** * Arithmetic and logical operations over machine integers *)
 
-Definition eq (x y: int) : bool := 
+Definition eq (x y: int) : bool :=
   if zeq (unsigned x) (unsigned y) then true else false.
 Definition lt (x y: int) : bool :=
   if zlt (signed x) (signed y) then true else false.
@@ -340,7 +340,7 @@ Definition Zshiftin (b: bool) (x: Z) : Z :=
 *)
 
 Definition Zzero_ext (n: Z) (x: Z) : Z :=
-  Z.iter n 
+  Z.iter n
     (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
     (fun x => 0)
     x.
@@ -410,8 +410,8 @@ Definition notbool  (x: int) : int  := if eq x zero then one else zero.
 Remark half_modulus_power:
   half_modulus = two_p (zwordsize - 1).
 Proof.
-  unfold half_modulus. rewrite modulus_power. 
-  set (ws1 := zwordsize - 1). 
+  unfold half_modulus. rewrite modulus_power.
+  set (ws1 := zwordsize - 1).
   replace (zwordsize) with (Zsucc ws1).
   rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega.
   unfold ws1. generalize wordsize_pos; omega.
@@ -420,8 +420,8 @@ Qed.
 
 Remark half_modulus_modulus: modulus = 2 * half_modulus.
 Proof.
-  rewrite half_modulus_power. rewrite modulus_power. 
-  rewrite <- two_p_S. apply f_equal. omega. 
+  rewrite half_modulus_power. rewrite modulus_power.
+  rewrite <- two_p_S. apply f_equal. omega.
   generalize wordsize_pos; omega.
 Qed.
 
@@ -454,8 +454,8 @@ Qed.
 Remark wordsize_max_unsigned: zwordsize <= max_unsigned.
 Proof.
   assert (zwordsize < modulus).
-    rewrite modulus_power. apply two_p_strict. 
-    generalize wordsize_pos. omega. 
+    rewrite modulus_power. apply two_p_strict.
+    generalize wordsize_pos. omega.
   unfold max_unsigned. omega.
 Qed.
 
@@ -468,14 +468,14 @@ Qed.
 
 Remark max_signed_unsigned: max_signed < max_unsigned.
 Proof.
-  unfold max_signed, max_unsigned. rewrite half_modulus_modulus. 
+  unfold max_signed, max_unsigned. rewrite half_modulus_modulus.
   generalize half_modulus_pos. omega.
 Qed.
 
 Lemma unsigned_repr_eq:
   forall x, unsigned (repr x) = Zmod x modulus.
 Proof.
-  intros. simpl. apply Z_mod_modulus_eq. 
+  intros. simpl. apply Z_mod_modulus_eq.
 Qed.
 
 Lemma signed_repr_eq:
@@ -528,14 +528,14 @@ 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. 
+  intros x y [k EQ]. subst x.
   rewrite Zplus_comm. apply Z_mod_plus. auto.
 Qed.
 
 Lemma eqmod_mod:
   forall x, eqmod x (x mod modul).
 Proof.
-  intros; red. exists (x / modul). 
+  intros; red. exists (x / modul).
   rewrite Zmult_comm. apply Z_div_mod_eq. auto.
 Qed.
 
@@ -549,7 +549,7 @@ 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. 
+  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring.
 Qed.
 
 Lemma eqmod_sub:
@@ -573,11 +573,11 @@ End EQ_MODULO.
 Lemma eqmod_divides:
   forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y.
 Proof.
-  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2]. 
+  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
   exists (k1*k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto.
-Qed. 
+Qed.
 
-(** We then specialize these definitions to equality modulo 
+(** We then specialize these definitions to equality modulo
   $2^{wordsize}$ #2<sup>wordsize</sup>#. *)
 
 Hint Resolve modulus_pos: ints.
@@ -630,7 +630,7 @@ Hint Resolve eqm_mult: ints.
 
 Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
 Proof.
-  intros. unfold repr. apply mkint_eq. 
+  intros. unfold repr. apply mkint_eq.
   rewrite !Z_mod_modulus_eq. apply eqmod_mod_eq. auto with ints. exact H.
 Qed.
 
@@ -644,7 +644,7 @@ Hint Resolve eqm_unsigned_repr: ints.
 Lemma eqm_unsigned_repr_l:
   forall a b, eqm a b -> eqm (unsigned (repr a)) b.
 Proof.
-  intros. apply eqm_trans with a. 
+  intros. apply eqm_trans with a.
   apply eqm_sym. apply eqm_unsigned_repr. auto.
 Qed.
 Hint Resolve eqm_unsigned_repr_l: ints.
@@ -653,7 +653,7 @@ Lemma eqm_unsigned_repr_r:
   forall a b, eqm a b -> eqm a (unsigned (repr b)).
 Proof.
   intros. apply eqm_trans with b. auto.
-  apply eqm_unsigned_repr. 
+  apply eqm_unsigned_repr.
 Qed.
 Hint Resolve eqm_unsigned_repr_r: ints.
 
@@ -662,7 +662,7 @@ Lemma eqm_signed_unsigned:
 Proof.
   intros; red. unfold signed. set (y := unsigned x).
   case (zlt y half_modulus); intro.
-  apply eqmod_refl. red; exists (-1); ring. 
+  apply eqmod_refl. red; exists (-1); ring.
 Qed.
 
 Theorem unsigned_range:
@@ -675,7 +675,7 @@ Hint Resolve unsigned_range: ints.
 Theorem unsigned_range_2:
   forall i, 0 <= unsigned i <= max_unsigned.
 Proof.
-  intro; unfold max_unsigned. 
+  intro; unfold max_unsigned.
   generalize (unsigned_range i). omega.
 Qed.
 Hint Resolve unsigned_range_2: ints.
@@ -683,13 +683,13 @@ Hint Resolve unsigned_range_2: ints.
 Theorem signed_range:
   forall i, min_signed <= signed i <= max_signed.
 Proof.
-  intros. unfold signed. 
+  intros. unfold signed.
   generalize (unsigned_range i). set (n := unsigned i). intros.
   case (zlt n half_modulus); intro.
   unfold max_signed. generalize min_signed_neg. omega.
   unfold min_signed, max_signed.
-  rewrite half_modulus_modulus in *. omega. 
-Qed.  
+  rewrite half_modulus_modulus in *. omega.
+Qed.
 
 Theorem repr_unsigned:
   forall i, repr (unsigned i) = i.
@@ -702,7 +702,7 @@ Hint Resolve repr_unsigned: ints.
 Lemma repr_signed:
   forall i, repr (signed i) = i.
 Proof.
-  intros. transitivity (repr (unsigned i)). 
+  intros. transitivity (repr (unsigned i)).
   apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
 Qed.
 Hint Resolve repr_signed: ints.
@@ -717,7 +717,7 @@ Qed.
 Theorem unsigned_repr:
   forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
 Proof.
-  intros. rewrite unsigned_repr_eq. 
+  intros. rewrite unsigned_repr_eq.
   apply Zmod_small. unfold max_unsigned in H. omega.
 Qed.
 Hint Resolve unsigned_repr: ints.
@@ -728,16 +728,16 @@ Proof.
   intros. unfold signed. destruct (zle 0 z).
   replace (unsigned (repr z)) with z.
   rewrite zlt_true. auto. unfold max_signed in H. omega.
-  symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega. 
+  symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega.
   pose (z' := z + modulus).
   replace (repr z) with (repr z').
   replace (unsigned (repr z')) with z'.
   rewrite zlt_false. unfold z'. omega.
   unfold z'. unfold min_signed in H.
-  rewrite half_modulus_modulus. omega. 
+  rewrite half_modulus_modulus. omega.
   symmetry. apply unsigned_repr.
   unfold z', max_unsigned. unfold min_signed, max_signed in H.
-  rewrite half_modulus_modulus. omega. 
+  rewrite half_modulus_modulus. omega.
   apply eqm_samerepr. unfold z'; red. exists 1. omega.
 Qed.
 
@@ -765,16 +765,16 @@ Qed.
 
 Theorem unsigned_one: unsigned one = 1.
 Proof.
-  unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega. 
-  unfold modulus. replace wordsize with (S(pred wordsize)). 
-  rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)). 
+  unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega.
+  unfold modulus. replace wordsize with (S(pred wordsize)).
+  rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)).
   omega.
-  generalize wordsize_pos. unfold zwordsize. omega. 
+  generalize wordsize_pos. unfold zwordsize. omega.
 Qed.
 
 Theorem unsigned_mone: unsigned mone = modulus - 1.
 Proof.
-  unfold mone; rewrite unsigned_repr_eq. 
+  unfold mone; rewrite unsigned_repr_eq.
   replace (-1) with ((modulus - 1) + (-1) * modulus).
   rewrite Z_mod_plus_full. apply Zmod_small.
   generalize modulus_pos. omega. omega.
@@ -789,12 +789,12 @@ Theorem signed_mone: signed mone = -1.
 Proof.
   unfold signed. rewrite unsigned_mone.
   rewrite zlt_false. omega.
-  rewrite half_modulus_modulus. generalize half_modulus_pos. omega.  
+  rewrite half_modulus_modulus. generalize half_modulus_pos. omega.
 Qed.
 
 Theorem one_not_zero: one <> zero.
 Proof.
-  assert (unsigned one <> unsigned zero). 
+  assert (unsigned one <> unsigned zero).
   rewrite unsigned_one; rewrite unsigned_zero; congruence.
   congruence.
 Qed.
@@ -802,7 +802,7 @@ Qed.
 Theorem unsigned_repr_wordsize:
   unsigned iwordsize = zwordsize.
 Proof.
-  unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. 
+  unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small.
   generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
 Qed.
 
@@ -820,7 +820,7 @@ Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y.
 Proof.
   intros; unfold eq. case (eq_dec x y); intro.
   subst y. rewrite zeq_true. auto.
-  rewrite zeq_false. auto. 
+  rewrite zeq_false. auto.
   destruct x; destruct y.
   simpl. red; intro. elim n. apply mkint_eq. auto.
 Qed.
@@ -838,11 +838,11 @@ Qed.
 Theorem eq_signed:
   forall x y, eq x y = if zeq (signed x) (signed y) then true else false.
 Proof.
-  intros. predSpec eq eq_spec x y. 
-  subst x. rewrite zeq_true; auto. 
+  intros. predSpec eq eq_spec x y.
+  subst x. rewrite zeq_true; auto.
   destruct (zeq (signed x) (signed y)); auto.
   elim H. rewrite <- (repr_signed x). rewrite <- (repr_signed y). congruence.
-Qed. 
+Qed.
 
 (** ** Properties of addition *)
 
@@ -851,7 +851,7 @@ Proof. intros; reflexivity.
 Qed.
 
 Theorem add_signed: forall x y, add x y = repr (signed x + signed y).
-Proof. 
+Proof.
   intros. rewrite add_unsigned. apply eqm_samerepr.
   apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned.
 Qed.
@@ -876,7 +876,7 @@ Proof.
   set (x' := unsigned x).
   set (y' := unsigned y).
   set (z' := unsigned z).
-  apply eqm_samerepr. 
+  apply eqm_samerepr.
   apply eqm_trans with ((x' + y') + z').
   auto with ints.
   rewrite <- Zplus_assoc. auto with ints.
@@ -884,7 +884,7 @@ Qed.
 
 Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
 Proof.
-  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. 
+  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
 Qed.
 
 Theorem add_neg_zero: forall x, add x (neg x) = zero.
@@ -901,19 +901,19 @@ Proof.
   intros.
   unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r.
   rewrite unsigned_repr_eq.
-  generalize (unsigned_range x) (unsigned_range y). intros. 
+  generalize (unsigned_range x) (unsigned_range y). intros.
   destruct (zlt (unsigned x + unsigned y) modulus).
-  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. 
-  rewrite unsigned_one. apply Zmod_unique with 1. omega. omega. 
-Qed. 
+  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
+  rewrite unsigned_one. apply Zmod_unique with 1. omega. omega.
+Qed.
 
 Corollary unsigned_add_either:
   forall x y,
   unsigned (add x y) = unsigned x + unsigned y
   \/ unsigned (add x y) = unsigned x + unsigned y - modulus.
 Proof.
-  intros. rewrite unsigned_add_carry. unfold add_carry. 
-  rewrite unsigned_zero. rewrite Zplus_0_r. 
+  intros. rewrite unsigned_add_carry. unfold add_carry.
+  rewrite unsigned_zero. rewrite Zplus_0_r.
   destruct (zlt (unsigned x + unsigned y) modulus).
   rewrite unsigned_zero. left; omega.
   rewrite unsigned_one. right; omega.
@@ -928,7 +928,7 @@ Qed.
 
 Theorem neg_zero: neg zero = zero.
 Proof.
-  unfold neg. rewrite unsigned_zero. auto. 
+  unfold neg. rewrite unsigned_zero. auto.
 Qed.
 
 Theorem neg_involutive: forall x, neg (neg x) = x.
@@ -936,7 +936,7 @@ Proof.
   intros; unfold neg.
   apply eqm_repr_eq. eapply eqm_trans. apply eqm_neg.
   apply eqm_unsigned_repr_l. apply eqm_refl. apply eqm_refl2. omega.
-Qed. 
+Qed.
 
 Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
 Proof.
@@ -952,7 +952,7 @@ Qed.
 
 Theorem sub_zero_l: forall x, sub x zero = x.
 Proof.
-  intros; unfold sub. rewrite unsigned_zero. 
+  intros; unfold sub. rewrite unsigned_zero.
   replace (unsigned x - 0) with (unsigned x) by omega. apply repr_unsigned.
 Qed.
 
@@ -974,7 +974,7 @@ Qed.
 
 Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y.
 Proof.
-  intros. repeat rewrite sub_add_opp. 
+  intros. repeat rewrite sub_add_opp.
   repeat rewrite add_assoc. decEq. apply add_commut.
 Qed.
 
@@ -989,7 +989,7 @@ Theorem sub_shifted:
   sub (add x z) (add y z) = sub x y.
 Proof.
   intros. rewrite sub_add_opp. rewrite neg_add_distr.
-  rewrite add_assoc. 
+  rewrite add_assoc.
   rewrite (add_commut (neg y) (neg z)).
   rewrite <- (add_assoc z). rewrite add_neg_zero.
   rewrite (add_commut zero). rewrite add_zero.
@@ -1010,22 +1010,22 @@ Proof.
   intros.
   unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r.
   rewrite unsigned_repr_eq.
-  generalize (unsigned_range x) (unsigned_range y). intros. 
+  generalize (unsigned_range x) (unsigned_range y). intros.
   destruct (zlt (unsigned x - unsigned y) 0).
-  rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega. 
-  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. 
-Qed. 
+  rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega.
+  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
+Qed.
 
 (** ** Properties of multiplication *)
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
 Proof.
-  intros; unfold mul. decEq. ring. 
+  intros; unfold mul. decEq. ring.
 Qed.
 
 Theorem mul_zero: forall x, mul x zero = zero.
 Proof.
-  intros; unfold mul. rewrite unsigned_zero. 
+  intros; unfold mul. rewrite unsigned_zero.
   unfold zero. decEq. ring.
 Qed.
 
@@ -1038,7 +1038,7 @@ Qed.
 
 Theorem mul_mone: forall x, mul x mone = neg x.
 Proof.
-  intros; unfold mul, neg. rewrite unsigned_mone. 
+  intros; unfold mul, neg. rewrite unsigned_mone.
   apply eqm_samerepr.
   replace (-unsigned x) with (0 - unsigned x) by omega.
   replace (unsigned x * (modulus - 1)) with (unsigned x * modulus - unsigned x) by ring.
@@ -1074,11 +1074,11 @@ Qed.
 Theorem mul_add_distr_r:
   forall x y z, mul x (add y z) = add (mul x y) (mul x z).
 Proof.
-  intros. rewrite mul_commut. rewrite mul_add_distr_l. 
+  intros. rewrite mul_commut. rewrite mul_add_distr_l.
   decEq; apply mul_commut.
-Qed. 
+Qed.
 
-Theorem neg_mul_distr_l: 
+Theorem neg_mul_distr_l:
   forall x y, neg(mul x y) = mul (neg x) y.
 Proof.
   intros. unfold mul, neg.
@@ -1093,7 +1093,7 @@ Theorem neg_mul_distr_r:
    forall x y, neg(mul x y) = mul x (neg y).
 Proof.
   intros. rewrite (mul_commut x y). rewrite (mul_commut x (neg y)).
-  apply neg_mul_distr_l. 
+  apply neg_mul_distr_l.
 Qed.
 
 Theorem mul_signed:
@@ -1109,13 +1109,13 @@ Lemma modu_divu_Euclid:
   forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).
 Proof.
   intros. unfold add, mul, divu, modu.
-  transitivity (repr (unsigned x)). auto with ints. 
-  apply eqm_samerepr. 
+  transitivity (repr (unsigned x)). auto with ints.
+  apply eqm_samerepr.
   set (x' := unsigned x). set (y' := unsigned y).
   apply eqm_trans with ((x' / y') * y' + x' mod y').
   apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq.
   generalize (unsigned_range y); intro.
-  assert (unsigned y <> 0). red; intro. 
+  assert (unsigned y <> 0). red; intro.
   elim H. rewrite <- (repr_unsigned y). unfold zero. congruence.
   unfold y'. omega.
   auto with ints.
@@ -1124,7 +1124,7 @@ Qed.
 Theorem modu_divu:
   forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).
 Proof.
-  intros. 
+  intros.
   assert (forall a b c, a = add b c -> c = sub a b).
   intros. subst a. rewrite sub_add_l. rewrite sub_idem.
   rewrite add_commut. rewrite add_zero. auto.
@@ -1135,20 +1135,20 @@ Lemma mods_divs_Euclid:
   forall x y, x = add (mul (divs x y) y) (mods x y).
 Proof.
   intros. unfold add, mul, divs, mods.
-  transitivity (repr (signed x)). auto with ints. 
-  apply eqm_samerepr. 
+  transitivity (repr (signed x)). auto with ints.
+  apply eqm_samerepr.
   set (x' := signed x). set (y' := signed y).
   apply eqm_trans with ((Z.quot x' y') * y' + Z.rem x' y').
   apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'.
   apply eqm_add; auto with ints.
-  apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints.  
-  unfold y'. apply eqm_signed_unsigned. 
+  apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints.
+  unfold y'. apply eqm_signed_unsigned.
 Qed.
 
 Theorem mods_divs:
   forall x y, mods x y = sub x (mul (divs x y) y).
 Proof.
-  intros. 
+  intros.
   assert (forall a b c, a = add b c -> c = sub a b).
   intros. subst a. rewrite sub_add_l. rewrite sub_idem.
   rewrite add_commut. rewrite add_zero. auto.
@@ -1171,26 +1171,26 @@ Qed.
 Theorem divs_mone:
   forall x, divs x mone = neg x.
 Proof.
-  unfold divs, neg; intros. 
-  rewrite signed_mone. 
+  unfold divs, neg; intros.
+  rewrite signed_mone.
   replace (Z.quot (signed x) (-1)) with (- (signed x)).
-  apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned. 
+  apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned.
   set (x' := signed x).
   set (one := 1).
   change (-1) with (- one). rewrite Zquot_opp_r.
-  assert (Z.quot x' one = x'). 
+  assert (Z.quot x' one = x').
   symmetry. apply Zquot_unique_full with 0. red.
-  change (Z.abs one) with 1. 
-  destruct (zle 0 x'). left. omega. right. omega. 
-  unfold one; ring. 
+  change (Z.abs one) with 1.
+  destruct (zle 0 x'). left. omega. right. omega.
+  unfold one; ring.
   congruence.
 Qed.
 
 Theorem mods_mone:
   forall x, mods x mone = zero.
 Proof.
-  intros. rewrite mods_divs. rewrite divs_mone. 
-  rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. 
+  intros. rewrite mods_divs. rewrite divs_mone.
+  rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem.
 Qed.
 
 (** ** Bit-level properties *)
@@ -1207,14 +1207,14 @@ Qed.
 
 Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true.
 Proof.
-  intros. destruct n; simpl; auto. 
+  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.succ_double_spec. omega.
   - rewrite Z.double_spec. omega.
 Qed.
 
@@ -1222,7 +1222,7 @@ 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. 
+  intros. rewrite !Zshiftin_spec in H.
   destruct b1; destruct b2.
   split; [auto|omega].
   omegaContradiction.
@@ -1235,7 +1235,7 @@ Remark Zdecomp:
 Proof.
   intros. destruct x; simpl.
   - auto.
-  - destruct p; auto. 
+  - destruct p; auto.
   - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto.
 Qed.
 
@@ -1265,7 +1265,7 @@ 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. 
+  intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto.
   omega. omega.
 Qed.
 
@@ -1273,19 +1273,19 @@ 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. 
+  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. 
+  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. 
+  intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto.
   omega. omega.
 Qed.
 
@@ -1296,14 +1296,14 @@ Lemma eqmod_same_bits:
 Proof.
   induction n; intros.
   - change (two_power_nat 0) with 1. exists (x-y); ring.
-  - rewrite two_power_nat_S. 
+  - 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 inj_S; omega. 
-      omega. omega. 
+      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega.
+      omega. omega.
   destruct H0 as [k EQ].
-  exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). 
+  exists k. rewrite (Zdecomp x). rewrite (Zdecomp y).
   replace (Z.odd y) with (Z.odd x).
-  rewrite EQ. rewrite !Zshiftin_spec. ring. 
+  rewrite EQ. rewrite !Zshiftin_spec. ring.
   exploit (H 0). rewrite inj_S; omega.
   rewrite !Ztestbit_base. auto.
 Qed.
@@ -1321,14 +1321,14 @@ Lemma same_bits_eqmod:
 Proof.
   induction n; intros.
   - simpl in H0. omegaContradiction.
-  - rewrite inj_S in H0. rewrite two_power_nat_S in H. 
-    rewrite !(Ztestbit_eq i); intuition. 
+  - rewrite inj_S 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. 
+      rewrite EQ. rewrite !Zshiftin_spec. ring.
     }
     exploit Zshiftin_inj; eauto. intros [A B].
     destruct (zeq i 0).
@@ -1348,8 +1348,8 @@ Remark two_power_nat_infinity:
 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. 
+  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:
@@ -1357,15 +1357,15 @@ Lemma equal_same_bits:
   (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
   x = y.
 Proof.
-  intros. 
+  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]. 
+  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. 
+    apply eqmod_same_bits. intros. apply H. tauto.
   assert (eqmod (two_power_nat n) z 0).
-    unfold z. destruct (zlt x y). 
+    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).
@@ -1377,13 +1377,13 @@ 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. 
+  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 !Ztestbit_shiftin; auto.
+  destruct (zeq i 0). auto. apply IND. omega.
   rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring.
 Qed.
 
@@ -1393,14 +1393,14 @@ Lemma Ztestbit_above:
   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. 
+  induction n; intros.
+  - change (two_power_nat 0) with 1 in H.
+    replace x with 0 by omega.
     apply Z.testbit_0_l.
   - rewrite inj_S 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. 
+    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:
@@ -1410,11 +1410,11 @@ Lemma Ztestbit_above_neg:
   Z.testbit x i = true.
 Proof.
   intros. set (y := -x-1).
-  assert (Z.testbit y i = false). 
-    apply Ztestbit_above with n. 
+  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. 
+  change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto.
   omega.
 Qed.
 
@@ -1423,17 +1423,17 @@ Lemma Zsign_bit:
   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. 
+  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 inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. 
-    rewrite IHn. rewrite two_power_nat_S. 
+  - rewrite inj_S. 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. 
+    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.
 
@@ -1443,7 +1443,7 @@ Lemma Zshiftin_ind:
   (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) ->
   forall x, 0 <= x -> P x.
 Proof.
-  intros. destruct x. 
+  intros. destruct x.
   - auto.
   - induction p.
     + change (P (Zshiftin true (Z.pos p))). auto.
@@ -1472,16 +1472,16 @@ Lemma Ztestbit_le:
   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. 
+  - 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 (Zsucc i)).
-        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. 
+        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
     }
-    rewrite (Zdecomp x0). rewrite !Zshiftin_spec. 
+    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. 
+    exploit (H1 0). omega. rewrite Ztestbit_base; auto.
     rewrite Ztestbit_shiftin_base. congruence.
 Qed.
 
@@ -1502,25 +1502,25 @@ Lemma same_bits_eq:
   (forall i, 0 <= i < zwordsize -> testbit x i = testbit y i) ->
   x = y.
 Proof.
-  intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y). 
+  intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y).
   apply eqm_samerepr. apply eqm_same_bits. auto.
 Qed.
 
 Lemma bits_above:
   forall x i, i >= zwordsize -> testbit x i = false.
 Proof.
-  intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range. 
-Qed. 
+  intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range.
+Qed.
 
 Lemma bits_zero:
   forall i, testbit zero i = false.
 Proof.
-  intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0. 
+  intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0.
 Qed.
 
 Remark bits_one: forall n, testbit one n = zeq n 0.
 Proof.
-  unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1. 
+  unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1.
 Qed.
 
 Lemma bits_mone:
@@ -1539,25 +1539,25 @@ Lemma sign_bit_of_unsigned:
 Proof.
   intros. unfold testbit.
   set (ws1 := pred wordsize).
-  assert (zwordsize - 1 = Z_of_nat ws1). 
-    unfold zwordsize, ws1, wordsize. 
+  assert (zwordsize - 1 = Z_of_nat ws1).
+    unfold zwordsize, ws1, wordsize.
     destruct WS.wordsize as [] eqn:E.
     elim WS.wordsize_not_zero; auto.
-    rewrite inj_S. simpl. omega. 
+    rewrite inj_S. simpl. omega.
   assert (half_modulus = two_power_nat ws1).
     rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power.
   rewrite H; rewrite H0.
-  apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0. 
+  apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0.
   rewrite <- half_modulus_modulus. apply unsigned_range.
 Qed.
-  
+
 Lemma bits_signed:
   forall x i, 0 <= i ->
   Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1).
 Proof.
   intros.
   destruct (zlt i zwordsize).
-  - apply same_bits_eqm. apply eqm_signed_unsigned. omega. 
+  - apply same_bits_eqm. apply eqm_signed_unsigned. omega.
   - unfold signed. rewrite sign_bit_of_unsigned. destruct (zlt (unsigned x) half_modulus).
     + apply Ztestbit_above with wordsize. apply unsigned_range. auto.
     + apply Ztestbit_above_neg with wordsize.
@@ -1569,11 +1569,11 @@ Lemma bits_le:
   (forall i, 0 <= i < zwordsize -> testbit x i = true -> testbit y i = true) ->
   unsigned x <= unsigned y.
 Proof.
-  intros. apply Ztestbit_le. generalize (unsigned_range y); omega. 
-  intros. fold (testbit y i). destruct (zlt i zwordsize). 
-  apply H. omega. auto. 
+  intros. apply Ztestbit_le. generalize (unsigned_range y); omega.
+  intros. fold (testbit y i). destruct (zlt i zwordsize).
+  apply H. omega. auto.
   fold (testbit x i) in H1. rewrite bits_above in H1; auto. congruence.
-Qed. 
+Qed.
 
 (** ** Properties of bitwise and, or, xor *)
 
@@ -1654,7 +1654,7 @@ Qed.
 
 Theorem or_zero: forall x, or x zero = x.
 Proof.
-  bit_solve. 
+  bit_solve.
 Qed.
 
 Corollary or_zero_l: forall x, or zero x = x.
@@ -1664,7 +1664,7 @@ Qed.
 
 Theorem or_mone: forall x, or x mone = mone.
 Proof.
-  bit_solve. 
+  bit_solve.
 Qed.
 
 Theorem or_idem: forall x, or x x = x.
@@ -1677,7 +1677,7 @@ Theorem and_or_distrib:
   and x (or y z) = or (and x y) (and x z).
 Proof.
   bit_solve. apply demorgan1.
-Qed.  
+Qed.
 
 Corollary and_or_distrib_l:
   forall x y z,
@@ -1690,8 +1690,8 @@ Theorem or_and_distrib:
   forall x y z,
   or x (and y z) = and (or x y) (or x z).
 Proof.
-  bit_solve. apply orb_andb_distrib_r. 
-Qed.  
+  bit_solve. apply orb_andb_distrib_r.
+Qed.
 
 Corollary or_and_distrib_l:
   forall x y z,
@@ -1702,7 +1702,7 @@ Qed.
 
 Theorem and_or_absorb: forall x y, and x (or x y) = x.
 Proof.
-  bit_solve. 
+  bit_solve.
   assert (forall a b, a && (a || b) = a) by destr_bool.
   auto.
 Qed.
@@ -1716,7 +1716,7 @@ Qed.
 
 Theorem xor_commut: forall x y, xor x y = xor y x.
 Proof.
-  bit_solve. apply xorb_comm. 
+  bit_solve. apply xorb_comm.
 Qed.
 
 Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
@@ -1726,7 +1726,7 @@ Qed.
 
 Theorem xor_zero: forall x, xor x zero = x.
 Proof.
-  bit_solve. apply xorb_false. 
+  bit_solve. apply xorb_false.
 Qed.
 
 Corollary xor_zero_l: forall x, xor zero x = x.
@@ -1736,7 +1736,7 @@ Qed.
 
 Theorem xor_idem: forall x, xor x x = zero.
 Proof.
-  bit_solve. apply xorb_nilpotent. 
+  bit_solve. apply xorb_nilpotent.
 Qed.
 
 Theorem xor_zero_one: xor zero one = one.
@@ -1747,7 +1747,7 @@ Proof. apply xor_idem. Qed.
 
 Theorem xor_zero_equal: forall x y, xor x y = zero -> x = y.
 Proof.
-  intros. apply same_bits_eq; intros. 
+  intros. apply same_bits_eq; intros.
   assert (xorb (testbit x i) (testbit y i) = false).
     rewrite <- bits_xor; auto. rewrite H. apply bits_zero.
   destruct (testbit x i); destruct (testbit y i); reflexivity || discriminate.
@@ -1757,23 +1757,23 @@ Theorem and_xor_distrib:
   forall x y z,
   and x (xor y z) = xor (and x y) (and x z).
 Proof.
-  bit_solve. 
+  bit_solve.
   assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)) by destr_bool.
   auto.
-Qed.  
+Qed.
 
 Theorem and_le:
   forall x y, unsigned (and x y) <= unsigned x.
 Proof.
-  intros. apply bits_le; intros. 
+  intros. apply bits_le; intros.
   rewrite bits_and in H0; auto. rewrite andb_true_iff in H0. tauto.
 Qed.
 
 Theorem or_le:
   forall x y, unsigned x <= unsigned (or x y).
 Proof.
-  intros. apply bits_le; intros. 
-  rewrite bits_or; auto. rewrite H0; auto. 
+  intros. apply bits_le; intros.
+  rewrite bits_or; auto. rewrite H0; auto.
 Qed.
 
 (** Properties of bitwise complement.*)
@@ -1781,7 +1781,7 @@ Qed.
 Theorem not_involutive:
   forall (x: int), not (not x) = x.
 Proof.
-  intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero. 
+  intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero.
 Qed.
 
 Theorem not_zero:
@@ -1799,31 +1799,31 @@ Qed.
 Theorem not_or_and_not:
   forall x y, not (or x y) = and (not x) (not y).
 Proof.
-  bit_solve. apply negb_orb. 
+  bit_solve. apply negb_orb.
 Qed.
 
 Theorem not_and_or_not:
   forall x y, not (and x y) = or (not x) (not y).
 Proof.
-  bit_solve. apply negb_andb. 
+  bit_solve. apply negb_andb.
 Qed.
 
 Theorem and_not_self:
   forall x, and x (not x) = zero.
 Proof.
-  bit_solve. 
+  bit_solve.
 Qed.
 
 Theorem or_not_self:
   forall x, or x (not x) = mone.
 Proof.
-  bit_solve. 
+  bit_solve.
 Qed.
 
 Theorem xor_not_self:
   forall x, xor x (not x) = mone.
 Proof.
-  bit_solve. destruct (testbit x i); auto. 
+  bit_solve. destruct (testbit x i); auto.
 Qed.
 
 Lemma unsigned_not:
@@ -1832,7 +1832,7 @@ Proof.
   intros. transitivity (unsigned (repr(-unsigned x - 1))).
   f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega.
   rewrite unsigned_repr_eq. apply Zmod_unique with (-1).
-  unfold max_unsigned. omega. 
+  unfold max_unsigned. omega.
   generalize (unsigned_range x). unfold max_unsigned. omega.
 Qed.
 
@@ -1840,30 +1840,30 @@ Theorem not_neg:
   forall x, not x = add (neg x) mone.
 Proof.
   bit_solve.
-  rewrite <- (repr_unsigned x) at 1. unfold add. 
+  rewrite <- (repr_unsigned x) at 1. unfold add.
   rewrite !testbit_repr; auto.
   transitivity (Z.testbit (-unsigned x - 1) i).
   symmetry. apply Z_one_complement. omega.
   apply same_bits_eqm; auto.
   replace (-unsigned x - 1) with (-unsigned x + (-1)) by omega.
-  apply eqm_add. 
-  unfold neg. apply eqm_unsigned_repr. 
-  rewrite unsigned_mone. exists (-1). ring. 
+  apply eqm_add.
+  unfold neg. apply eqm_unsigned_repr.
+  rewrite unsigned_mone. exists (-1). ring.
 Qed.
 
 Theorem neg_not:
   forall x, neg x = add (not x) one.
 Proof.
-  intros. rewrite not_neg. rewrite add_assoc. 
-  replace (add mone one) with zero. rewrite add_zero. auto. 
-  apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one. 
-  exists (-1). ring. 
+  intros. rewrite not_neg. rewrite add_assoc.
+  replace (add mone one) with zero. rewrite add_zero. auto.
+  apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one.
+  exists (-1). ring.
 Qed.
 
 Theorem sub_add_not:
   forall x y, sub x y = add (add x (not y)) one.
 Proof.
-  intros. rewrite sub_add_opp. rewrite neg_not. 
+  intros. rewrite sub_add_opp. rewrite neg_not.
   rewrite ! add_assoc. auto.
 Qed.
 
@@ -1883,13 +1883,13 @@ Theorem sub_borrow_add_carry:
   b = zero \/ b = one ->
   sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.
 Proof.
-  intros. unfold sub_borrow, add_carry. rewrite unsigned_not. 
+  intros. unfold sub_borrow, add_carry. rewrite unsigned_not.
   replace (unsigned (xor b one)) with (1 - unsigned b).
   destruct (zlt (unsigned x - unsigned y - unsigned b)).
   rewrite zlt_true. rewrite xor_zero_l; auto.
   unfold max_unsigned; omega.
   rewrite zlt_false. rewrite xor_idem; auto.
-  unfold max_unsigned; omega. 
+  unfold max_unsigned; omega.
   destruct H; subst b.
   rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto.
   rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto.
@@ -1908,14 +1908,14 @@ Proof.
   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. 
+    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. 
+    + apply IND. omega. intros.
+      exploit (EXCL (Z.succ j)). omega.
       rewrite !Ztestbit_shiftin_succ. auto.
       omega. omega.
 Qed.
@@ -1926,8 +1926,8 @@ Theorem add_is_or:
   add x y = or x y.
 Proof.
   bit_solve. unfold add. rewrite testbit_repr; auto.
-  apply Z_add_is_or. omega. 
-  intros. 
+  apply Z_add_is_or. omega.
+  intros.
   assert (testbit (and x y) j = testbit zero j) by congruence.
   autorewrite with ints in H2. assumption. omega.
 Qed.
@@ -1935,9 +1935,9 @@ Qed.
 Theorem xor_is_or:
   forall x y, and x y = zero -> xor x y = or x y.
 Proof.
-  bit_solve. 
+  bit_solve.
   assert (testbit (and x y) i = testbit zero i) by congruence.
-  autorewrite with ints in H1; auto. 
+  autorewrite with ints in H1; auto.
   destruct (testbit x i); destruct (testbit y i); simpl in *; congruence.
 Qed.
 
@@ -1957,8 +1957,8 @@ Proof.
   intros. rewrite add_is_or.
   rewrite and_or_distrib; auto.
   rewrite (and_commut x y).
-  rewrite and_assoc. 
-  repeat rewrite <- (and_assoc x). 
+  rewrite and_assoc.
+  repeat rewrite <- (and_assoc x).
   rewrite (and_commut (and x x)).
   rewrite <- and_assoc.
   rewrite H. rewrite and_commut. apply and_zero.
@@ -1972,8 +1972,8 @@ Lemma bits_shl:
   testbit (shl x y) i =
   if zlt i (unsigned y) then false else testbit x (i - unsigned y).
 Proof.
-  intros. unfold shl. rewrite testbit_repr; auto. 
-  destruct (zlt i (unsigned y)). 
+  intros. unfold shl. rewrite testbit_repr; auto.
+  destruct (zlt i (unsigned y)).
   apply Z.shiftl_spec_low. auto.
   apply Z.shiftl_spec_high. omega. omega.
 Qed.
@@ -1984,11 +1984,11 @@ Lemma bits_shru:
   testbit (shru x y) i =
   if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false.
 Proof.
-  intros. unfold shru. rewrite testbit_repr; auto. 
+  intros. unfold shru. rewrite testbit_repr; auto.
   rewrite Z.shiftr_spec. fold (testbit x (i + unsigned y)).
   destruct (zlt (i + unsigned y) zwordsize).
   auto.
-  apply bits_above; auto. 
+  apply bits_above; auto.
   omega.
 Qed.
 
@@ -1998,8 +1998,8 @@ Lemma bits_shr:
   testbit (shr x y) i =
   testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1).
 Proof.
-  intros. unfold shr. rewrite testbit_repr; auto. 
-  rewrite Z.shiftr_spec. apply bits_signed. 
+  intros. unfold shr. rewrite testbit_repr; auto.
+  rewrite Z.shiftr_spec. apply bits_signed.
   generalize (unsigned_range y); omega.
   omega.
 Qed.
@@ -2017,10 +2017,10 @@ Lemma bitwise_binop_shl:
   f' false false = false ->
   f (shl x n) (shl y n) = shl (f x y) n.
 Proof.
-  intros. apply same_bits_eq; intros. 
+  intros. apply same_bits_eq; intros.
   rewrite H; auto. rewrite !bits_shl; auto.
   destruct (zlt i (unsigned n)); auto.
-  rewrite H; auto. generalize (unsigned_range n); omega. 
+  rewrite H; auto. generalize (unsigned_range n); omega.
 Qed.
 
 Theorem and_shl:
@@ -2060,22 +2060,22 @@ Qed.
 
 Theorem shl_shl:
   forall x y z,
-  ltu y iwordsize = true -> 
+  ltu y iwordsize = true ->
   ltu z iwordsize = true ->
   ltu (add y z) iwordsize = true ->
   shl (shl x y) z = shl x (add y z).
 Proof.
-  intros. 
+  intros.
   generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
   assert (unsigned (add y z) = unsigned y + unsigned z).
-    unfold add. apply unsigned_repr. 
+    unfold add. apply unsigned_repr.
     generalize two_wordsize_max_unsigned; omega.
-  apply same_bits_eq; intros. 
+  apply same_bits_eq; intros.
   rewrite bits_shl; auto.
   destruct (zlt i (unsigned z)).
   - rewrite bits_shl; auto. rewrite zlt_true. auto. omega.
   - rewrite bits_shl. destruct (zlt (i - unsigned z) (unsigned y)).
-    + rewrite bits_shl; auto. rewrite zlt_true. auto. omega. 
+    + rewrite bits_shl; auto. rewrite zlt_true. auto. omega.
     + rewrite bits_shl; auto. rewrite zlt_false. f_equal. omega. omega.
     + omega.
 Qed.
@@ -2091,10 +2091,10 @@ Lemma bitwise_binop_shru:
   f' false false = false ->
   f (shru x n) (shru y n) = shru (f x y) n.
 Proof.
-  intros. apply same_bits_eq; intros. 
+  intros. apply same_bits_eq; intros.
   rewrite H; auto. rewrite !bits_shru; auto.
   destruct (zlt (i + unsigned n) zwordsize); auto.
-  rewrite H; auto. generalize (unsigned_range n); omega. 
+  rewrite H; auto. generalize (unsigned_range n); omega.
 Qed.
 
 Theorem and_shru:
@@ -2120,7 +2120,7 @@ Qed.
 
 Theorem shru_shru:
   forall x y z,
-  ltu y iwordsize = true -> 
+  ltu y iwordsize = true ->
   ltu z iwordsize = true ->
   ltu (add y z) iwordsize = true ->
   shru (shru x y) z = shru x (add y z).
@@ -2128,14 +2128,14 @@ Proof.
   intros.
   generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
   assert (unsigned (add y z) = unsigned y + unsigned z).
-    unfold add. apply unsigned_repr. 
+    unfold add. apply unsigned_repr.
     generalize two_wordsize_max_unsigned; omega.
-  apply same_bits_eq; intros. 
+  apply same_bits_eq; intros.
   rewrite bits_shru; auto.
   destruct (zlt (i + unsigned z) zwordsize).
   - rewrite bits_shru. destruct (zlt (i + unsigned z + unsigned y) zwordsize).
-    + rewrite bits_shru; auto. rewrite zlt_true. f_equal. omega. omega.  
-    + rewrite bits_shru; auto. rewrite zlt_false. auto. omega. 
+    + rewrite bits_shru; auto. rewrite zlt_true. f_equal. omega. omega.
+    + rewrite bits_shru; auto. rewrite zlt_false. auto. omega.
     + omega.
   - rewrite bits_shru; auto. rewrite zlt_false. auto. omega.
 Qed.
@@ -2150,10 +2150,10 @@ Lemma bitwise_binop_shr:
   (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
   f (shr x n) (shr y n) = shr (f x y) n.
 Proof.
-  intros. apply same_bits_eq; intros. 
+  intros. apply same_bits_eq; intros.
   rewrite H; auto. rewrite !bits_shr; auto.
-  rewrite H; auto. 
-  destruct (zlt (i + unsigned n) zwordsize). 
+  rewrite H; auto.
+  destruct (zlt (i + unsigned n) zwordsize).
   generalize (unsigned_range n); omega.
   omega.
 Qed.
@@ -2181,7 +2181,7 @@ Qed.
 
 Theorem shr_shr:
   forall x y z,
-  ltu y iwordsize = true -> 
+  ltu y iwordsize = true ->
   ltu z iwordsize = true ->
   ltu (add y z) iwordsize = true ->
   shr (shr x y) z = shr x (add y z).
@@ -2189,14 +2189,14 @@ Proof.
   intros.
   generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
   assert (unsigned (add y z) = unsigned y + unsigned z).
-    unfold add. apply unsigned_repr. 
+    unfold add. apply unsigned_repr.
     generalize two_wordsize_max_unsigned; omega.
-  apply same_bits_eq; intros. 
+  apply same_bits_eq; intros.
   rewrite !bits_shr; auto. f_equal.
   destruct (zlt (i + unsigned z) zwordsize).
-  rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by omega. auto. 
+  rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by omega. auto.
   rewrite (zlt_false _ (i + unsigned (add y z))).
-  destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega. 
+  destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega.
   omega.
   destruct (zlt (i + unsigned z) zwordsize); omega.
 Qed.
@@ -2217,8 +2217,8 @@ Theorem shr_and_shru_and:
   shru (shl z y) y = z ->
   and (shr x y) z = and (shru x y) z.
 Proof.
-  intros. 
-  rewrite <- H. 
+  intros.
+  rewrite <- H.
   rewrite and_shru. rewrite and_shr_shru. auto.
 Qed.
 
@@ -2228,19 +2228,19 @@ Theorem shru_lt_zero:
 Proof.
   intros. apply same_bits_eq; intros.
   rewrite bits_shru; auto.
-  rewrite unsigned_repr. 
+  rewrite unsigned_repr.
   destruct (zeq i 0).
   subst i. rewrite Zplus_0_l. rewrite zlt_true.
   rewrite sign_bit_of_unsigned.
-  unfold lt. rewrite signed_zero. unfold signed. 
+  unfold lt. rewrite signed_zero. unfold signed.
   destruct (zlt (unsigned x) half_modulus).
-  rewrite zlt_false. auto. generalize (unsigned_range x); omega. 
-  rewrite zlt_true. unfold one; rewrite testbit_repr; auto. 
-  generalize (unsigned_range x); omega. 
+  rewrite zlt_false. auto. generalize (unsigned_range x); omega.
+  rewrite zlt_true. unfold one; rewrite testbit_repr; auto.
+  generalize (unsigned_range x); omega.
   omega.
   rewrite zlt_false.
-  unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. 
-  destruct (lt x zero). 
+  unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false.
+  destruct (lt x zero).
   rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto.
   rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto.
   auto. omega. omega.
@@ -2256,10 +2256,10 @@ Proof.
   rewrite unsigned_repr.
   transitivity (testbit x (zwordsize - 1)).
   f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega.
-  rewrite sign_bit_of_unsigned. 
-  unfold lt. rewrite signed_zero. unfold signed. 
+  rewrite sign_bit_of_unsigned.
+  unfold lt. rewrite signed_zero. unfold signed.
   destruct (zlt (unsigned x) half_modulus).
-  rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. 
+  rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega.
   rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega.
   generalize wordsize_max_unsigned; omega.
 Qed.
@@ -2267,18 +2267,18 @@ Qed.
 (** ** Properties of rotations *)
 
 Lemma bits_rol:
-  forall x y i, 
+  forall x y i,
   0 <= i < zwordsize ->
   testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize).
 Proof.
   intros. unfold rol.
-  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. 
-  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). 
+  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos.
+  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize).
   intros EQ.
-  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. 
+  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos.
   fold j. intros RANGE.
   rewrite testbit_repr; auto.
-  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. 
+  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega.
   destruct (zlt i j).
   - rewrite Z.shiftl_spec_low; auto. simpl.
     unfold testbit. f_equal.
@@ -2289,9 +2289,9 @@ Proof.
     fold (testbit x (i + (zwordsize - j))).
     rewrite bits_above. rewrite orb_false_r.
     fold (testbit x (i - j)).
-    f_equal. symmetry. apply Zmod_unique with (-k). 
+    f_equal. symmetry. apply Zmod_unique with (-k).
     rewrite EQ. ring.
-    omega. omega. omega. omega. 
+    omega. omega. omega. omega.
 Qed.
 
 Lemma bits_ror:
@@ -2300,26 +2300,26 @@ Lemma bits_ror:
   testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize).
 Proof.
   intros. unfold ror.
-  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. 
-  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). 
+  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos.
+  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize).
   intros EQ.
-  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. 
+  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos.
   fold j. intros RANGE.
   rewrite testbit_repr; auto.
-  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. 
+  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega.
   destruct (zlt (i + j) zwordsize).
-  - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r. 
+  - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r.
     unfold testbit. f_equal.
     symmetry. apply Zmod_unique with k.
     rewrite EQ. ring.
     omega. omega.
   - rewrite Z.shiftl_spec_high.
-    fold (testbit x (i + j)). 
-    rewrite bits_above. simpl. 
-    unfold testbit. f_equal. 
-    symmetry. apply Zmod_unique with (k + 1). 
+    fold (testbit x (i + j)).
+    rewrite bits_above. simpl.
+    unfold testbit. f_equal.
+    symmetry. apply Zmod_unique with (k + 1).
     rewrite EQ. ring.
-    omega. omega. omega. omega. 
+    omega. omega. omega. omega.
 Qed.
 
 Hint Rewrite bits_rol bits_ror: ints.
@@ -2330,13 +2330,13 @@ Theorem shl_rolm:
   shl x n = rolm x n (shl mone n).
 Proof.
   intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
-  unfold rolm. apply same_bits_eq; intros. 
-  rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto. 
+  unfold rolm. apply same_bits_eq; intros.
+  rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto.
   destruct (zlt i (unsigned n)).
   - rewrite andb_false_r; auto.
-  - generalize (unsigned_range n); intros. 
-    rewrite bits_mone. rewrite andb_true_r. f_equal. 
-    symmetry. apply Zmod_small. omega. 
+  - generalize (unsigned_range n); intros.
+    rewrite bits_mone. rewrite andb_true_r. f_equal.
+    symmetry. apply Zmod_small. omega.
     omega.
 Qed.
 
@@ -2346,15 +2346,15 @@ Theorem shru_rolm:
   shru x n = rolm x (sub iwordsize n) (shru mone n).
 Proof.
   intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
-  unfold rolm. apply same_bits_eq; intros. 
-  rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto. 
+  unfold rolm. apply same_bits_eq; intros.
+  rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto.
   destruct (zlt (i + unsigned n) zwordsize).
-  - generalize (unsigned_range n); intros. 
+  - generalize (unsigned_range n); intros.
     rewrite bits_mone. rewrite andb_true_r. f_equal.
     unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize.
-    symmetry. apply Zmod_unique with (-1). ring. omega. 
+    symmetry. apply Zmod_unique with (-1). ring. omega.
     rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. omega.
-    omega. 
+    omega.
   - rewrite andb_false_r; auto.
 Qed.
 
@@ -2362,8 +2362,8 @@ Theorem rol_zero:
   forall x,
   rol x zero = x.
 Proof.
-  bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r. 
-  apply Zmod_small; auto. 
+  bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r.
+  apply Zmod_small; auto.
 Qed.
 
 Lemma bitwise_binop_rol:
@@ -2371,8 +2371,8 @@ Lemma bitwise_binop_rol:
   (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
   rol (f x y) n = f (rol x n) (rol y n).
 Proof.
-  intros. apply same_bits_eq; intros. 
-  rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto. 
+  intros. apply same_bits_eq; intros.
+  rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto.
   apply Z_mod_lt. apply wordsize_pos.
 Qed.
 
@@ -2402,11 +2402,11 @@ Theorem rol_rol:
   Zdivide zwordsize modulus ->
   rol (rol x n) m = rol x (modu (add n m) iwordsize).
 Proof.
-  bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos. 
+  bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos.
   set (M := unsigned m); set (N := unsigned n).
   apply eqmod_trans with (i - M - N).
   apply eqmod_sub.
-  apply eqmod_sym. apply eqmod_mod. apply wordsize_pos. 
+  apply eqmod_sym. apply eqmod_mod. apply wordsize_pos.
   apply eqmod_refl.
   replace (i - M - N) with (i - (M + N)) by omega.
   apply eqmod_sub.
@@ -2416,8 +2416,8 @@ Proof.
   unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize.
   assert (forall a, eqmod zwordsize a (unsigned (repr a))).
     intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption.
-  eapply eqmod_trans. 2: apply H1. 
-  apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto. 
+  eapply eqmod_trans. 2: apply H1.
+  apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto.
   apply Z_mod_lt. apply wordsize_pos.
 Qed.
 
@@ -2436,7 +2436,7 @@ Theorem rolm_rolm:
            (and (rol m1 n2) m2).
 Proof.
   intros.
-  unfold rolm. rewrite rol_and. rewrite and_assoc. 
+  unfold rolm. rewrite rol_and. rewrite and_assoc.
   rewrite rol_rol. reflexivity. auto.
 Qed.
 
@@ -2444,7 +2444,7 @@ Theorem or_rolm:
   forall x n m1 m2,
   or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).
 Proof.
-  intros; unfold rolm. symmetry. apply and_or_distrib. 
+  intros; unfold rolm. symmetry. apply and_or_distrib.
 Qed.
 
 Theorem ror_rol:
@@ -2455,23 +2455,23 @@ Proof.
   intros.
   generalize (ltu_iwordsize_inv _ H); intros.
   apply same_bits_eq; intros.
-  rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal. 
+  rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal.
   unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize.
-  apply eqmod_mod_eq. apply wordsize_pos. exists 1. ring. 
-  rewrite unsigned_repr_wordsize. 
-  generalize wordsize_pos; generalize wordsize_max_unsigned; omega. 
+  apply eqmod_mod_eq. apply wordsize_pos. exists 1. ring.
+  rewrite unsigned_repr_wordsize.
+  generalize wordsize_pos; generalize wordsize_max_unsigned; omega.
 Qed.
 
 Theorem ror_rol_neg:
   forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y).
 Proof.
   intros. apply same_bits_eq; intros.
-  rewrite bits_ror by auto. rewrite bits_rol by auto. 
-  f_equal. apply eqmod_mod_eq. omega. 
-  apply eqmod_trans with (i - (- unsigned y)). 
-  apply eqmod_refl2; omega. 
+  rewrite bits_ror by auto. rewrite bits_rol by auto.
+  f_equal. apply eqmod_mod_eq. omega.
+  apply eqmod_trans with (i - (- unsigned y)).
+  apply eqmod_refl2; omega.
   apply eqmod_sub. apply eqmod_refl.
-  apply eqmod_divides with modulus. 
+  apply eqmod_divides with modulus.
   apply eqm_unsigned_repr. auto.
 Qed.
 
@@ -2484,17 +2484,17 @@ Theorem or_ror:
 Proof.
   intros.
   generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
-  unfold ror, or, shl, shru. apply same_bits_eq; intros. 
-  rewrite !testbit_repr; auto. 
+  unfold ror, or, shl, shru. apply same_bits_eq; intros.
+  rewrite !testbit_repr; auto.
   rewrite !Z.lor_spec. rewrite orb_comm. f_equal; apply same_bits_eqm; auto.
   - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal.
-    rewrite Zmod_small; auto. 
-    assert (unsigned (add y z) = zwordsize). 
-      rewrite H1. apply unsigned_repr_wordsize. 
-    unfold add in H5. rewrite unsigned_repr in H5. 
-    omega. 
-    generalize two_wordsize_max_unsigned; omega. 
-  - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. 
+    rewrite Zmod_small; auto.
+    assert (unsigned (add y z) = zwordsize).
+      rewrite H1. apply unsigned_repr_wordsize.
+    unfold add in H5. rewrite unsigned_repr in H5.
+    omega.
+    generalize two_wordsize_max_unsigned; omega.
+  - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal.
     apply Zmod_small; auto.
 Qed.
 
@@ -2509,23 +2509,23 @@ Fixpoint powerserie (l: list Z): Z :=
 Lemma Z_one_bits_powerserie:
   forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
 Proof.
-  assert (forall n x i, 
+  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. 
+  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. 
+    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. 
+  rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec.
   destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring.
-  omega. omega. 
+  omega. omega.
   }
   intros. rewrite <- H. change (two_p 0) with 1. omega.
   omega. exact H0.
@@ -2543,7 +2543,7 @@ Proof.
   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. 
+  intros [A|B]. subst j. omega. auto.
   auto.
   }
   intros. generalize (H wordsize x 0 i H0). fold zwordsize; omega.
@@ -2572,7 +2572,7 @@ Theorem is_power2_range:
 Proof.
   intros. unfold ltu. rewrite unsigned_repr_wordsize.
   apply zlt_true. generalize (is_power2_rng _ _ H). tauto.
-Qed. 
+Qed.
 
 Lemma is_power2_correct:
   forall n logn,
@@ -2589,7 +2589,7 @@ Proof.
   rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
   auto. omega. elim (H z); intros.
   generalize wordsize_max_unsigned; omega.
-  auto with coqlib. 
+  auto with coqlib.
   intros; discriminate.
 Qed.
 
@@ -2600,9 +2600,9 @@ Remark two_p_range:
 Proof.
   intros. split.
   assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
-  generalize (two_p_monotone_strict _ _ H). 
-  unfold zwordsize; rewrite <- two_power_nat_two_p. 
-  unfold max_unsigned, modulus. omega. 
+  generalize (two_p_monotone_strict _ _ H).
+  unfold zwordsize; rewrite <- two_power_nat_two_p.
+  unfold max_unsigned, modulus. omega.
 Qed.
 
 Remark Z_one_bits_zero:
@@ -2617,7 +2617,7 @@ Remark Z_one_bits_two_p:
   Z_one_bits n (two_p x) i = (i + x) :: nil.
 Proof.
   induction n; intros; simpl. simpl in H. omegaContradiction.
-  rewrite inj_S in H. 
+  rewrite inj_S 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)).
@@ -2631,7 +2631,7 @@ Lemma is_power2_two_p:
   forall n, 0 <= n < zwordsize ->
   is_power2 (repr (two_p n)) = Some (repr n).
 Proof.
-  intros. unfold is_power2. rewrite unsigned_repr. 
+  intros. unfold is_power2. rewrite unsigned_repr.
   rewrite Z_one_bits_two_p. auto. auto.
   apply two_p_range. auto.
 Qed.
@@ -2645,7 +2645,7 @@ Lemma Zshiftl_mul_two_p:
 Proof.
   intros. destruct n; simpl.
   - omega.
-  - pattern p. apply Pos.peano_ind. 
+  - 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.
@@ -2658,7 +2658,7 @@ Lemma shl_mul_two_p:
   shl x y = mul x (repr (two_p (unsigned y))).
 Proof.
   intros. unfold shl, mul. apply eqm_samerepr.
-  rewrite Zshiftl_mul_two_p. auto with ints. 
+  rewrite Zshiftl_mul_two_p. auto with ints.
   generalize (unsigned_range y); omega.
 Qed.
 
@@ -2666,7 +2666,7 @@ Theorem shl_mul:
   forall x y,
   shl x y = mul x (shl one y).
 Proof.
-  intros. 
+  intros.
   assert (shl one y = repr (two_p (unsigned y))).
   {
     rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto.
@@ -2690,21 +2690,21 @@ Theorem shifted_or_is_add:
   unsigned y < two_p n ->
   or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y).
 Proof.
-  intros. rewrite <- add_is_or. 
-  - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints. 
+  intros. rewrite <- add_is_or.
+  - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints.
     rewrite shl_mul_two_p. unfold mul. apply eqm_unsigned_repr_l.
-    apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l. 
-    apply eqm_refl2. rewrite unsigned_repr. auto. 
+    apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l.
+    apply eqm_refl2. rewrite unsigned_repr. auto.
     generalize wordsize_max_unsigned; omega.
   - bit_solve.
-    rewrite unsigned_repr. 
+    rewrite unsigned_repr.
     destruct (zlt i n).
     + auto.
-    + replace (testbit y i) with false. apply andb_false_r. 
+    + replace (testbit y i) with false. apply andb_false_r.
       symmetry. unfold testbit.
       assert (EQ: Z.of_nat (Z.to_nat n) = n) by (apply Z2Nat.id; omega).
       apply Ztestbit_above with (Z.to_nat n).
-      rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0. 
+      rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0.
       generalize (unsigned_range y); omega.
       rewrite EQ; auto.
     + generalize wordsize_max_unsigned; omega.
@@ -2717,8 +2717,8 @@ Lemma Zshiftr_div_two_p:
 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. 
+  - 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.
@@ -2731,7 +2731,7 @@ Lemma shru_div_two_p:
   forall x y,
   shru x y = repr (unsigned x / two_p (unsigned y)).
 Proof.
-  intros. unfold shru. 
+  intros. unfold shru.
   rewrite Zshiftr_div_two_p. auto.
   generalize (unsigned_range y); omega.
 Qed.
@@ -2775,12 +2775,12 @@ Lemma Ztestbit_mod_two_p:
   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. 
+  - 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)) 
+  - 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 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.
@@ -2800,10 +2800,10 @@ 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)). 
+  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. 
+  apply Zmod_unique with (-1). ring.
+  exploit (two_p_gt_ZERO n). auto. omega.
 Qed.
 
 Theorem modu_and:
@@ -2814,12 +2814,12 @@ Proof.
   intros. generalize (is_power2_correct _ _ H); intro.
   generalize (is_power2_rng _ _ H); intro.
   apply same_bits_eq; intros.
-  rewrite bits_and; auto. 
+  rewrite bits_and; auto.
   unfold sub. rewrite testbit_repr; auto.
-  rewrite H0. rewrite unsigned_one. 
+  rewrite H0. rewrite unsigned_one.
   unfold modu. rewrite testbit_repr; auto. rewrite H0.
-  rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1. 
-  destruct (zlt i (unsigned logn)). 
+  rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1.
+  destruct (zlt i (unsigned logn)).
   rewrite andb_true_r; auto.
   rewrite andb_false_r; auto.
   tauto. tauto. tauto. tauto.
@@ -2834,11 +2834,11 @@ Lemma Zquot_Zdiv:
 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. 
+     + 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. 
+       rewrite <- Z_div_mod_eq. ring. auto. ring.
   - apply Zquot_Zdiv_pos; omega.
 Qed.
 
@@ -2850,20 +2850,20 @@ Proof.
   intros.
   set (uy := unsigned y).
   assert (0 <= uy < zwordsize - 1).
-    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. 
+    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
     generalize wordsize_pos wordsize_max_unsigned; omega.
-  rewrite shr_div_two_p. unfold shrx. unfold divs.  
+  rewrite shr_div_two_p. unfold shrx. unfold divs.
   assert (shl one y = repr (two_p uy)).
     transitivity (mul one (repr (two_p uy))).
-    symmetry. apply mul_pow2. replace y with (repr uy). 
+    symmetry. apply mul_pow2. replace y with (repr uy).
     apply is_power2_two_p. omega. apply repr_unsigned.
     rewrite mul_commut. apply mul_one.
   assert (two_p uy > 0). apply two_p_gt_ZERO. omega.
-  assert (two_p uy < half_modulus). 
-    rewrite half_modulus_power. 
+  assert (two_p uy < half_modulus).
+    rewrite half_modulus_power.
     apply two_p_monotone_strict. auto.
   assert (two_p uy < modulus).
-    rewrite modulus_power. apply two_p_monotone_strict. omega. 
+    rewrite modulus_power. apply two_p_monotone_strict. omega.
   assert (unsigned (shl one y) = two_p uy).
     rewrite H1. apply unsigned_repr. unfold max_unsigned. omega.
   assert (signed (shl one y) = two_p uy).
@@ -2871,15 +2871,15 @@ Proof.
     unfold max_signed. generalize min_signed_neg. omega.
   rewrite H6.
   rewrite Zquot_Zdiv; auto.
-  unfold lt. rewrite signed_zero.  
+  unfold lt. rewrite signed_zero.
   destruct (zlt (signed x) 0); auto.
   rewrite add_signed.
   assert (signed (sub (shl one y) one) = two_p uy - 1).
-    unfold sub. rewrite H5. rewrite unsigned_one.  
+    unfold sub. rewrite H5. rewrite unsigned_one.
     apply signed_repr.
-    generalize min_signed_neg. unfold max_signed. omega. 
+    generalize min_signed_neg. unfold max_signed. omega.
   rewrite H7. rewrite signed_repr. f_equal. f_equal. omega.
-  generalize (signed_range x). intros.  
+  generalize (signed_range x). intros.
   assert (two_p uy - 1 <= max_signed). unfold max_signed. omega. omega.
 Qed.
 
@@ -2888,27 +2888,27 @@ Theorem shrx_shr_2:
   ltu y (repr (zwordsize - 1)) = true ->
   shrx x y = shr (add x (shru (shr x (repr (zwordsize - 1))) (sub iwordsize y))) y.
 Proof.
-  intros. 
+  intros.
   rewrite shrx_shr by auto. f_equal.
   rewrite shr_lt_zero. destruct (lt x zero).
 - set (uy := unsigned y).
   generalize (unsigned_range y); fold uy; intros.
   assert (0 <= uy < zwordsize - 1).
-    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. 
+    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
     generalize wordsize_pos wordsize_max_unsigned; omega.
   assert (two_p uy < modulus).
-    rewrite modulus_power. apply two_p_monotone_strict. omega. 
+    rewrite modulus_power. apply two_p_monotone_strict. omega.
   f_equal. rewrite shl_mul_two_p. fold uy. rewrite mul_commut. rewrite mul_one.
-  unfold sub. rewrite unsigned_one. rewrite unsigned_repr. 
-  rewrite unsigned_repr_wordsize. fold uy. 
-  apply same_bits_eq; intros. rewrite bits_shru by auto. 
+  unfold sub. rewrite unsigned_one. rewrite unsigned_repr.
+  rewrite unsigned_repr_wordsize. fold uy.
+  apply same_bits_eq; intros. rewrite bits_shru by auto.
   rewrite testbit_repr by auto. rewrite Ztestbit_two_p_m1 by omega.
   rewrite unsigned_repr by (generalize wordsize_max_unsigned; omega).
-  destruct (zlt i uy). 
+  destruct (zlt i uy).
   rewrite zlt_true by omega. rewrite bits_mone by omega. auto.
   rewrite zlt_false by omega. auto.
   assert (two_p uy > 0) by (apply two_p_gt_ZERO; omega). unfold max_unsigned; omega.
-- replace (shru zero (sub iwordsize y)) with zero. 
+- replace (shru zero (sub iwordsize y)) with zero.
   rewrite add_zero; auto.
   bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto.
 Qed.
@@ -2917,9 +2917,9 @@ Lemma Zdiv_shift:
   forall x y, y > 0 ->
   (x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1.
 Proof.
-  intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H).  
+  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). 
+  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.
@@ -2930,8 +2930,8 @@ Theorem shrx_carry:
   shrx x y = add (shr x y) (shr_carry x y).
 Proof.
   intros. rewrite shrx_shr; auto. unfold shr_carry.
-  unfold lt. set (sx := signed x). rewrite signed_zero. 
-  destruct (zlt sx 0); simpl. 
+  unfold lt. set (sx := signed x). rewrite signed_zero.
+  destruct (zlt sx 0); simpl.
   2: rewrite add_zero; auto.
   set (uy := unsigned y).
   assert (0 <= uy < zwordsize - 1).
@@ -2943,46 +2943,46 @@ Proof.
     symmetry. rewrite H1. apply modu_and with (logn := y).
     rewrite is_power2_two_p. unfold uy. rewrite repr_unsigned. auto.
     omega.
-  rewrite H2. rewrite H1. 
+  rewrite H2. rewrite H1.
   repeat rewrite shr_div_two_p. fold sx. fold uy.
   assert (two_p uy > 0). apply two_p_gt_ZERO. omega.
   assert (two_p uy < modulus).
     rewrite modulus_power. apply two_p_monotone_strict. omega.
-  assert (two_p uy < half_modulus). 
-    rewrite half_modulus_power. 
+  assert (two_p uy < half_modulus).
+    rewrite half_modulus_power.
     apply two_p_monotone_strict. auto.
   assert (two_p uy < modulus).
     rewrite modulus_power. apply two_p_monotone_strict. omega.
   assert (sub (repr (two_p uy)) one = repr (two_p uy - 1)).
-    unfold sub. apply eqm_samerepr. apply eqm_sub. apply eqm_sym; apply eqm_unsigned_repr. 
+    unfold sub. apply eqm_samerepr. apply eqm_sub. apply eqm_sym; apply eqm_unsigned_repr.
     rewrite unsigned_one. apply eqm_refl.
   rewrite H7. rewrite add_signed. fold sx.
-  rewrite (signed_repr (two_p uy - 1)). rewrite signed_repr. 
-  unfold modu. rewrite unsigned_repr. 
-  unfold eq. rewrite unsigned_zero. rewrite unsigned_repr. 
+  rewrite (signed_repr (two_p uy - 1)). rewrite signed_repr.
+  unfold modu. rewrite unsigned_repr.
+  unfold eq. rewrite unsigned_zero. rewrite unsigned_repr.
   assert (unsigned x mod two_p uy = sx mod two_p uy).
-    apply eqmod_mod_eq; auto. apply eqmod_divides with modulus. 
+    apply eqmod_mod_eq; auto. apply eqmod_divides with modulus.
     fold eqm. unfold sx. apply eqm_sym. apply eqm_signed_unsigned.
-    unfold modulus. rewrite two_power_nat_two_p. 
+    unfold modulus. rewrite two_power_nat_two_p.
     exists (two_p (zwordsize - uy)). rewrite <- two_p_is_exp.
     f_equal. fold zwordsize; omega. omega. omega.
   rewrite H8. rewrite Zdiv_shift; auto.
-  unfold add. apply eqm_samerepr. apply eqm_add. 
-  apply eqm_unsigned_repr. 
+  unfold add. apply eqm_samerepr. apply eqm_add.
+  apply eqm_unsigned_repr.
   destruct (zeq (sx mod two_p uy) 0); simpl.
   rewrite unsigned_zero. apply eqm_refl.
   rewrite unsigned_one. apply eqm_refl.
   generalize (Z_mod_lt (unsigned x) (two_p uy) H3). unfold max_unsigned. omega.
   unfold max_unsigned; omega.
-  generalize (signed_range x). fold sx. intros. split. omega. unfold max_signed. omega. 
-  generalize min_signed_neg. unfold max_signed. omega. 
+  generalize (signed_range x). fold sx. intros. split. omega. unfold max_signed. omega.
+  generalize min_signed_neg. unfold max_signed. omega.
 Qed.
 
 (** Connections between [shr] and [shru]. *)
 
 Lemma shr_shru_positive:
   forall x y,
-  signed x >= 0 -> 
+  signed x >= 0 ->
   shr x y = shru x y.
 Proof.
   intros.
@@ -2996,7 +2996,7 @@ Proof.
   intros.
   assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega.
   generalize (sign_bit_of_unsigned y). rewrite zlt_true; auto. intros A.
-  generalize (sign_bit_of_unsigned (and x y)). rewrite bits_and. rewrite A. 
+  generalize (sign_bit_of_unsigned (and x y)). rewrite bits_and. rewrite A.
   rewrite andb_false_r. unfold signed.
   destruct (zlt (unsigned (and x y)) half_modulus).
   intros. generalize (unsigned_range (and x y)); omega.
@@ -3008,7 +3008,7 @@ Theorem shr_and_is_shru_and:
   forall x y z,
   lt y zero = false -> shr (and x y) z = shru (and x y) z.
 Proof.
-  intros. apply shr_shru_positive. apply and_positive. 
+  intros. apply shr_shru_positive. apply and_positive.
   unfold lt in H. rewrite signed_zero in H. destruct (zlt (signed y) 0). congruence. auto.
 Qed.
 
@@ -3017,14 +3017,14 @@ Qed.
 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. 
+  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. 
+  intros. destruct n; simpl.
   - auto.
   - rewrite Pos.add_1_r. apply Pos.iter_succ.
   - compute in H. elim H; auto.
@@ -3037,7 +3037,7 @@ Lemma Znatlike_ind:
   forall n, P n.
 Proof.
   intros. destruct (zle 0 n).
-  apply natlike_ind; auto. apply H; omega. 
+  apply natlike_ind; auto. apply H; omega.
   apply H. omega.
 Qed.
 
@@ -3045,12 +3045,12 @@ 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. 
+  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. 
+  - 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).
@@ -3059,12 +3059,12 @@ Proof.
       omega.
 Qed.
 
-Lemma bits_zero_ext: 
+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.
 Proof.
   intros. unfold zero_ext. destruct (zlt i zwordsize).
-  rewrite testbit_repr; auto. rewrite Zzero_ext_spec. auto. auto. 
+  rewrite testbit_repr; auto. rewrite Zzero_ext_spec. auto. auto.
   rewrite !bits_above; auto. destruct (zlt i n); auto.
 Qed.
 
@@ -3072,20 +3072,20 @@ 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. 
+  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. 
+    + 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. 
+      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). 
+      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.
@@ -3097,13 +3097,13 @@ Proof.
   - omega.
 Qed.
 
-Lemma bits_sign_ext: 
+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).
 Proof.
   intros. unfold sign_ext.
   rewrite testbit_repr; auto. rewrite Zsign_ext_spec. destruct (zlt i n); auto.
-  omega. auto. 
+  omega. auto.
 Qed.
 
 Hint Rewrite bits_zero_ext bits_sign_ext: ints.
@@ -3119,7 +3119,7 @@ Theorem sign_ext_above:
   forall n x, n >= zwordsize -> sign_ext n x = x.
 Proof.
   intros. apply same_bits_eq; intros.
-  unfold sign_ext; rewrite testbit_repr; auto. 
+  unfold sign_ext; rewrite testbit_repr; auto.
   rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. omega.
 Qed.
 
@@ -3127,22 +3127,22 @@ Theorem zero_ext_and:
   forall n x, 0 <= n -> zero_ext n x = and x (repr (two_p n - 1)).
 Proof.
   bit_solve. rewrite testbit_repr; auto. rewrite Ztestbit_two_p_m1; intuition.
-  destruct (zlt i n). 
-  rewrite andb_true_r; auto. 
+  destruct (zlt i n).
+  rewrite andb_true_r; auto.
   rewrite andb_false_r; auto.
   tauto.
 Qed.
 
 Theorem zero_ext_mod:
-  forall n x, 0 <= n < zwordsize -> 
+  forall n x, 0 <= n < zwordsize ->
   unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n).
 Proof.
   intros. apply equal_same_bits. intros.
   rewrite Ztestbit_mod_two_p; auto.
-  fold (testbit (zero_ext n x) i). 
+  fold (testbit (zero_ext n x) i).
   destruct (zlt i zwordsize).
   rewrite bits_zero_ext; auto.
-  rewrite bits_above. rewrite zlt_false; auto. omega. omega. 
+  rewrite bits_above. rewrite zlt_false; auto. omega. omega.
   omega.
 Qed.
 
@@ -3150,8 +3150,8 @@ Theorem zero_ext_widen:
   forall x n n', 0 <= n <= n' ->
   zero_ext n' (zero_ext n x) = zero_ext n x.
 Proof.
-  bit_solve. destruct (zlt i n). 
-  apply zlt_true. omega. 
+  bit_solve. destruct (zlt i n).
+  apply zlt_true. omega.
   destruct (zlt i n'); auto.
   tauto. tauto.
 Qed.
@@ -3163,11 +3163,11 @@ Proof.
   intros. destruct (zlt n' zwordsize).
   bit_solve. destruct (zlt i n').
   auto.
-  rewrite (zlt_false _ i n). 
+  rewrite (zlt_false _ i n).
   destruct (zlt (n' - 1) n); f_equal; omega.
   omega. omega.
   destruct (zlt i n'); omega.
-  omega. omega. 
+  omega. omega.
   apply sign_ext_above; auto.
 Qed.
 
@@ -3176,10 +3176,10 @@ Theorem sign_zero_ext_widen:
   sign_ext n' (zero_ext n x) = zero_ext n x.
 Proof.
   intros. destruct (zlt n' zwordsize).
-  bit_solve. 
+  bit_solve.
   destruct (zlt i n').
   auto.
-  rewrite !zlt_false. auto. omega. omega. omega. 
+  rewrite !zlt_false. auto. omega. omega. omega.
   destruct (zlt i n'); omega.
   omega.
   apply sign_ext_above; auto.
@@ -3189,8 +3189,8 @@ Theorem zero_ext_narrow:
   forall x n n', 0 <= n <= n' ->
   zero_ext n (zero_ext n' x) = zero_ext n x.
 Proof.
-  bit_solve. destruct (zlt i n). 
-  apply zlt_true. omega. 
+  bit_solve. destruct (zlt i n).
+  apply zlt_true. omega.
   auto.
   omega. omega. omega.
 Qed.
@@ -3201,10 +3201,10 @@ Theorem sign_ext_narrow:
 Proof.
   intros. destruct (zlt n zwordsize).
   bit_solve. destruct (zlt i n); f_equal; apply zlt_true; omega.
-  omega. 
+  omega.
   destruct (zlt i n); omega.
   omega. omega.
-  rewrite (sign_ext_above n'). auto. omega.  
+  rewrite (sign_ext_above n'). auto. omega.
 Qed.
 
 Theorem zero_sign_ext_narrow:
@@ -3212,7 +3212,7 @@ Theorem zero_sign_ext_narrow:
   zero_ext n (sign_ext n' x) = zero_ext n x.
 Proof.
   intros. destruct (zlt n' zwordsize).
-  bit_solve. 
+  bit_solve.
   destruct (zlt i n); auto.
   rewrite zlt_true; auto. omega.
   omega. omega. omega.
@@ -3235,10 +3235,10 @@ Theorem sign_ext_zero_ext:
   forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x.
 Proof.
   intros. destruct (zlt n zwordsize).
-  bit_solve. 
-  destruct (zlt i n). 
+  bit_solve.
+  destruct (zlt i n).
   rewrite zlt_true; auto.
-  rewrite zlt_true; auto. omega. 
+  rewrite zlt_true; auto. omega.
   destruct (zlt i n); omega.
   rewrite zero_ext_above; auto.
 Qed.
@@ -3268,12 +3268,12 @@ Proof.
   assert (unsigned y = zwordsize - n).
     unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
   apply same_bits_eq; intros.
-  rewrite bits_zero_ext. 
+  rewrite bits_zero_ext.
   rewrite bits_shru; auto.
   destruct (zlt i n).
-  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. 
-  omega. omega. omega. 
-  rewrite zlt_false. auto. omega. 
+  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
+  omega. omega. omega.
+  rewrite zlt_false. auto. omega.
   omega.
 Qed.
 
@@ -3287,13 +3287,13 @@ Proof.
   assert (unsigned y = zwordsize - n).
     unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
   apply same_bits_eq; intros.
-  rewrite bits_sign_ext. 
+  rewrite bits_sign_ext.
   rewrite bits_shr; auto.
   destruct (zlt i n).
-  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. 
-  omega. omega. omega. 
-  rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega. 
-  omega. omega. omega. omega. omega. 
+  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
+  omega. omega. omega.
+  rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
+  omega. omega. omega. omega. omega.
 Qed.
 
 (** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n]
@@ -3302,13 +3302,13 @@ Qed.
 Lemma zero_ext_range:
   forall n x, 0 <= n < zwordsize -> 0 <= unsigned (zero_ext n x) < two_p n.
 Proof.
-  intros. rewrite zero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega. 
+  intros. rewrite zero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega.
 Qed.
 
 Lemma eqmod_zero_ext:
   forall n x, 0 <= n < zwordsize -> eqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x).
 Proof.
-  intros. rewrite zero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod. 
+  intros. rewrite zero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod.
   apply two_p_gt_ZERO. omega.
 Qed.
 
@@ -3318,25 +3318,25 @@ Qed.
 Lemma sign_ext_range:
   forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1).
 Proof.
-  intros. rewrite sign_ext_shr_shl; auto. 
+  intros. rewrite sign_ext_shr_shl; auto.
   set (X := shl x (repr (zwordsize - n))).
   assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; omega).
   assert (unsigned (repr (zwordsize - n)) = zwordsize - n).
-    apply unsigned_repr. 
+    apply unsigned_repr.
     split. omega. generalize wordsize_max_unsigned; omega.
   rewrite shr_div_two_p.
   rewrite signed_repr.
   rewrite H1.
-  apply Zdiv_interval_1. 
+  apply Zdiv_interval_1.
   omega. omega. apply two_p_gt_ZERO; omega.
   replace (- two_p (n - 1) * two_p (zwordsize - n))
      with (- (two_p (n - 1) * two_p (zwordsize - n))) by ring.
   rewrite <- two_p_is_exp.
   replace (n - 1 + (zwordsize - n)) with (zwordsize - 1) by omega.
   rewrite <- half_modulus_power.
-  generalize (signed_range X). unfold min_signed, max_signed. omega. 
+  generalize (signed_range X). unfold min_signed, max_signed. omega.
   omega. omega.
-  apply Zdiv_interval_2. apply signed_range. 
+  apply Zdiv_interval_2. apply signed_range.
   generalize min_signed_neg; omega.
   generalize max_signed_pos; omega.
   rewrite H1. apply two_p_gt_ZERO. omega.
@@ -3346,13 +3346,13 @@ Lemma eqmod_sign_ext':
   forall n x, 0 < n < zwordsize ->
   eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x).
 Proof.
-  intros. 
+  intros.
   set (N := Z.to_nat n).
   assert (Z.of_nat N = n) by (apply Z2Nat.id; omega).
-  rewrite <- H0. rewrite <- two_power_nat_two_p. 
-  apply eqmod_same_bits; intros. 
-  rewrite H0 in H1. rewrite H0. 
-  fold (testbit (sign_ext n x) i). rewrite bits_sign_ext. 
+  rewrite <- H0. rewrite <- two_power_nat_two_p.
+  apply eqmod_same_bits; intros.
+  rewrite H0 in H1. rewrite H0.
+  fold (testbit (sign_ext n x) i). rewrite bits_sign_ext.
   rewrite zlt_true. auto. omega. omega. omega.
 Qed.
 
@@ -3360,11 +3360,11 @@ Lemma eqmod_sign_ext:
   forall n x, 0 < n < zwordsize ->
   eqmod (two_p n) (signed (sign_ext n x)) (unsigned x).
 Proof.
-  intros. apply eqmod_trans with (unsigned (sign_ext n x)). 
-  apply eqmod_divides with modulus. apply eqm_signed_unsigned. 
-  exists (two_p (zwordsize - n)). 
+  intros. apply eqmod_trans with (unsigned (sign_ext n x)).
+  apply eqmod_divides with modulus. apply eqm_signed_unsigned.
+  exists (two_p (zwordsize - n)).
   unfold modulus. rewrite two_power_nat_two_p. fold zwordsize.
-  rewrite <- two_p_is_exp. f_equal. omega. omega. omega. 
+  rewrite <- two_p_is_exp. f_equal. omega. omega. omega.
   apply eqmod_sign_ext'; auto.
 Qed.
 
@@ -3374,8 +3374,8 @@ Theorem one_bits_range:
   forall x i, In i (one_bits x) -> ltu i iwordsize = true.
 Proof.
   assert (A: forall p, 0 <= p < zwordsize -> ltu (repr p) iwordsize = true).
-    intros. unfold ltu, iwordsize. apply zlt_true. 
-    repeat rewrite unsigned_repr. tauto. 
+    intros. unfold ltu, iwordsize. apply zlt_true.
+    repeat rewrite unsigned_repr. tauto.
     generalize wordsize_max_unsigned; omega.
     generalize wordsize_max_unsigned; omega.
   intros. unfold one_bits in H.
@@ -3392,21 +3392,21 @@ Fixpoint int_of_one_bits (l: list int) : int :=
 Theorem one_bits_decomp:
   forall x, x = int_of_one_bits (one_bits x).
 Proof.
-  intros. 
+  intros.
   transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))).
   transitivity (repr (unsigned x)).
   auto with ints. decEq. apply Z_one_bits_powerserie.
   auto with ints.
-  unfold one_bits. 
+  unfold one_bits.
   generalize (Z_one_bits_range (unsigned x)).
   generalize (Z_one_bits wordsize (unsigned x) 0).
   induction l.
   intros; reflexivity.
   intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr.
-  apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. 
-  rewrite mul_one. apply eqm_unsigned_repr_r. 
+  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 _ _)). generalize wordsize_max_unsigned. omega.
   auto with ints.
   intros; apply H; auto with coqlib.
 Qed.
@@ -3443,7 +3443,7 @@ Lemma translate_eq:
 Proof.
   intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
   unfold add. rewrite e. apply zeq_true.
-  apply zeq_false. unfold add. red; intro. apply n. 
+  apply zeq_false. unfold add. red; intro. apply n.
   apply eqm_small_eq; auto with ints.
   replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d).
   replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d).
@@ -3473,7 +3473,7 @@ Theorem translate_cmpu:
 Proof.
   intros. unfold cmpu.
   rewrite translate_eq. repeat rewrite translate_ltu; auto.
-Qed.  
+Qed.
 
 Lemma translate_lt:
   forall x y d,
@@ -3495,13 +3495,13 @@ Theorem translate_cmp:
 Proof.
   intros. unfold cmp.
   rewrite translate_eq. repeat rewrite translate_lt; auto.
-Qed.  
+Qed.
 
 Theorem notbool_isfalse_istrue:
   forall x, is_false x -> is_true (notbool x).
 Proof.
-  unfold is_false, is_true, notbool; intros; subst x. 
-  rewrite eq_true. apply one_not_zero. 
+  unfold is_false, is_true, notbool; intros; subst x.
+  rewrite eq_true. apply one_not_zero.
 Qed.
 
 Theorem notbool_istrue_isfalse:
@@ -3527,7 +3527,7 @@ Theorem lt_sub_overflow:
   forall x y,
   xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.
 Proof.
-  intros. unfold negative, sub_overflow, lt. rewrite sub_signed. 
+  intros. unfold negative, sub_overflow, lt. rewrite sub_signed.
   rewrite signed_zero. rewrite Zminus_0_r.
   generalize (signed_range x) (signed_range y).
   set (X := signed x); set (Y := signed y). intros RX RY.
@@ -3540,19 +3540,19 @@ Proof.
   + unfold proj_sumbool; rewrite zle_true by omega.
     rewrite signed_repr. rewrite zlt_false by omega. apply xor_idem.
     unfold min_signed, max_signed; omega.
-  + unfold proj_sumbool; rewrite zle_false by omega. 
+  + unfold proj_sumbool; rewrite zle_false by omega.
     replace (signed (repr (X - Y))) with (X - Y - modulus).
-    rewrite zlt_true by omega. apply xor_idem. 
-    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y). 
-    rewrite zlt_false; auto. 
+    rewrite zlt_true by omega. apply xor_idem.
+    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y).
+    rewrite zlt_false; auto.
     symmetry. apply Zmod_unique with 0; omega.
 - unfold proj_sumbool at 2. rewrite zle_true at 1 by omega. rewrite andb_true_r.
   rewrite (zlt_true _ X) by omega.
   destruct (zlt (X - Y) (-half_modulus)).
-  + unfold proj_sumbool; rewrite zle_false by omega. 
+  + unfold proj_sumbool; rewrite zle_false by omega.
     replace (signed (repr (X - Y))) with (X - Y + modulus).
     rewrite zlt_false by omega. apply xor_zero.
-    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus). 
+    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus).
     rewrite zlt_true by omega; auto.
     symmetry. apply Zmod_unique with (-1); omega.
   + unfold proj_sumbool; rewrite zle_true by omega.
@@ -3573,8 +3573,8 @@ Lemma no_overlap_sound:
   unsigned (add base ofs1) + sz1 <= unsigned (add base ofs2)
   \/ unsigned (add base ofs2) + sz2 <= unsigned (add base ofs1).
 Proof.
-  intros. 
-  destruct (andb_prop _ _ H1). clear H1. 
+  intros.
+  destruct (andb_prop _ _ H1). clear H1.
   destruct (andb_prop _ _ H2). clear H2.
   exploit proj_sumbool_true. eexact H1. intro A; clear H1.
   exploit proj_sumbool_true. eexact H4. intro B; clear H4.
@@ -3610,18 +3610,18 @@ Lemma Zsize_shiftin:
   forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x).
 Proof.
   intros. destruct x; compute in H; try discriminate.
-  destruct b. 
+  destruct b.
   change (Zshiftin true (Zpos p)) with (Zpos (p~1)).
-  simpl. f_equal. rewrite Pos.add_1_r; auto. 
+  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. 
+  simpl. f_equal. rewrite Pos.add_1_r; auto.
 Qed.
 
 Lemma Ztestbit_size_1:
   forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true.
 Proof.
   intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto.
-  intros. rewrite Zsize_shiftin; 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.
@@ -3629,14 +3629,14 @@ 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. 
+  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. 
+    + 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. 
+      rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega.
       omega. omega.
     + omega.
 Qed.
@@ -3644,25 +3644,25 @@ Qed.
 Lemma Zsize_interval_1:
   forall x, 0 <= x -> 0 <= x < two_p (Zsize x).
 Proof.
-  intros. 
+  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. 
+    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). 
+  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. 
+  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 (Zpred (Zsize x))). auto. omega. 
+  exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega.
   rewrite Ztestbit_size_1. congruence. omega.
 Qed.
 
@@ -3670,15 +3670,15 @@ Lemma Zsize_monotone:
   forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
 Proof.
   intros. apply Zge_le. apply Zsize_interval_2. apply Zsize_pos.
-  exploit (Zsize_interval_1 y). omega. 
-  omega. 
+  exploit (Zsize_interval_1 y). omega.
+  omega.
 Qed.
 
 Theorem size_zero: size zero = 0.
 Proof.
   unfold size; rewrite unsigned_zero; auto.
 Qed.
-  
+
 Theorem bits_size_1:
   forall x, x = zero \/ testbit x (Zpred (size x)) = true.
 Proof.
@@ -3690,8 +3690,8 @@ Qed.
 Theorem bits_size_2:
   forall x i, size x <= i -> testbit x i = false.
 Proof.
-  intros. apply Ztestbit_size_2. generalize (unsigned_range x); omega. 
-  fold (size x); omega. 
+  intros. apply Ztestbit_size_2. generalize (unsigned_range x); omega.
+  fold (size x); omega.
 Qed.
 
 Theorem size_range:
@@ -3700,9 +3700,9 @@ Proof.
   intros; split. apply Zsize_pos.
   destruct (bits_size_1 x).
   subst x; unfold size; rewrite unsigned_zero; simpl. generalize wordsize_pos; omega.
-  destruct (zle (size x) zwordsize); auto. 
+  destruct (zle (size x) zwordsize); auto.
   rewrite bits_above in H. congruence. omega.
-Qed. 
+Qed.
 
 Theorem bits_size_3:
   forall x n,
@@ -3710,10 +3710,10 @@ Theorem bits_size_3:
   (forall i, n <= i < zwordsize -> testbit x i = false) ->
   size x <= n.
 Proof.
-  intros. destruct (zle (size x) n). auto. 
-  destruct (bits_size_1 x). 
+  intros. destruct (zle (size x) n). auto.
+  destruct (bits_size_1 x).
   subst x. unfold size; rewrite unsigned_zero; assumption.
-  rewrite (H0 (Z.pred (size x))) in H1. congruence. 
+  rewrite (H0 (Z.pred (size x))) in H1. congruence.
   generalize (size_range x); omega.
 Qed.
 
@@ -3728,7 +3728,7 @@ Proof.
   assert (size x <= n).
     apply bits_size_3; auto.
   destruct (zlt (size x) n).
-  rewrite bits_size_2 in H0. congruence. omega. 
+  rewrite bits_size_2 in H0. congruence. omega.
   omega.
 Qed.
 
@@ -3747,24 +3747,24 @@ Qed.
 Theorem size_and:
   forall a b, size (and a b) <= Z.min (size a) (size b).
 Proof.
-  intros. 
+  intros.
   assert (0 <= Z.min (size a) (size b)).
-    generalize (size_range a) (size_range b). zify; omega. 
+    generalize (size_range a) (size_range b). zify; omega.
   apply bits_size_3. auto. intros.
-  rewrite bits_and. zify. subst z z0. destruct H1. 
-  rewrite (bits_size_2 a). auto. omega. 
-  rewrite (bits_size_2 b). apply andb_false_r. omega. 
+  rewrite bits_and. zify. subst z z0. destruct H1.
+  rewrite (bits_size_2 a). auto. omega.
+  rewrite (bits_size_2 b). apply andb_false_r. omega.
   omega.
 Qed.
 
 Corollary and_interval:
   forall a b, 0 <= unsigned (and a b) < two_p (Z.min (size a) (size b)).
 Proof.
-  intros. 
-  generalize (size_interval_1 (and a b)); intros. 
+  intros.
+  generalize (size_interval_1 (and a b)); intros.
   assert (two_p (size (and a b)) <= two_p (Z.min (size a) (size b))).
-  apply two_p_monotone. split. generalize (size_range (and a b)); omega. 
-  apply size_and. 
+  apply two_p_monotone. split. generalize (size_range (and a b)); omega.
+  apply size_and.
   omega.
 Qed.
 
@@ -3776,42 +3776,42 @@ Proof.
   subst a. rewrite size_zero. rewrite or_zero_l. zify; omega.
   destruct (bits_size_1 b).
   subst b. rewrite size_zero. rewrite or_zero. zify; omega.
-  zify. destruct H3 as [[P Q] | [P Q]]; subst. 
-  apply bits_size_4. tauto. rewrite bits_or. rewrite H2. apply orb_true_r. 
-  omega. 
-  intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. 
-  apply bits_size_4. tauto. rewrite bits_or. rewrite H1. apply orb_true_l. 
+  zify. destruct H3 as [[P Q] | [P Q]]; subst.
+  apply bits_size_4. tauto. rewrite bits_or. rewrite H2. apply orb_true_r.
+  omega.
+  intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega.
+  apply bits_size_4. tauto. rewrite bits_or. rewrite H1. apply orb_true_l.
   destruct (zeq (size a) 0). unfold testbit in H1. rewrite Z.testbit_neg_r in H1.
-  congruence. omega. omega. 
-  intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. 
+  congruence. omega. omega.
+  intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega.
 Qed.
 
 Corollary or_interval:
   forall a b, 0 <= unsigned (or a b) < two_p (Z.max (size a) (size b)).
 Proof.
-  intros. rewrite <- size_or. apply size_interval_1. 
+  intros. rewrite <- size_or. apply size_interval_1.
 Qed.
 
 Theorem size_xor:
   forall a b, size (xor a b) <= Z.max (size a) (size b).
 Proof.
-  intros. 
+  intros.
   assert (0 <= Z.max (size a) (size b)).
-    generalize (size_range a) (size_range b). zify; omega. 
+    generalize (size_range a) (size_range b). zify; omega.
   apply bits_size_3. auto. intros.
-  rewrite bits_xor. rewrite !bits_size_2. auto. 
+  rewrite bits_xor. rewrite !bits_size_2. auto.
+  zify; omega.
   zify; omega.
-  zify; omega. 
-  omega. 
+  omega.
 Qed.
 
 Corollary xor_interval:
   forall a b, 0 <= unsigned (xor a b) < two_p (Z.max (size a) (size b)).
 Proof.
-  intros. 
-  generalize (size_interval_1 (xor a b)); intros. 
+  intros.
+  generalize (size_interval_1 (xor a b)); intros.
   assert (two_p (size (xor a b)) <= two_p (Z.max (size a) (size b))).
-  apply two_p_monotone. split. generalize (size_range (xor a b)); omega. 
+  apply two_p_monotone. split. generalize (size_range (xor a b)); omega.
   apply size_xor.
   omega.
 Qed.
@@ -3837,7 +3837,7 @@ Notation int := Int.int.
 Remark int_wordsize_divides_modulus:
   Zdivide (Z_of_nat Int.wordsize) Int.modulus.
 Proof.
-  exists (two_p (32-5)); reflexivity. 
+  exists (two_p (32-5)); reflexivity.
 Qed.
 
 Module Wordsize_8.
@@ -3883,8 +3883,8 @@ Lemma bits_shl':
   testbit (shl' x y) i =
   if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y).
 Proof.
-  intros. unfold shl'. rewrite testbit_repr; auto. 
-  destruct (zlt i (Int.unsigned y)). 
+  intros. unfold shl'. rewrite testbit_repr; auto.
+  destruct (zlt i (Int.unsigned y)).
   apply Z.shiftl_spec_low. auto.
   apply Z.shiftl_spec_high. omega. omega.
 Qed.
@@ -3895,11 +3895,11 @@ Lemma bits_shru':
   testbit (shru' x y) i =
   if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false.
 Proof.
-  intros. unfold shru'. rewrite testbit_repr; auto. 
+  intros. unfold shru'. rewrite testbit_repr; auto.
   rewrite Z.shiftr_spec. fold (testbit x (i + Int.unsigned y)).
   destruct (zlt (i + Int.unsigned y) zwordsize).
   auto.
-  apply bits_above; auto. 
+  apply bits_above; auto.
   omega.
 Qed.
 
@@ -3909,8 +3909,8 @@ Lemma bits_shr':
   testbit (shr' x y) i =
   testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1).
 Proof.
-  intros. unfold shr'. rewrite testbit_repr; auto. 
-  rewrite Z.shiftr_spec. apply bits_signed. 
+  intros. unfold shr'. rewrite testbit_repr; auto.
+  rewrite Z.shiftr_spec. apply bits_signed.
   generalize (Int.unsigned_range y); omega.
   omega.
 Qed.
@@ -3927,7 +3927,7 @@ Definition ofwords (hi lo: Int.int) : int :=
 Lemma bits_loword:
   forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i.
 Proof.
-  intros. unfold loword. rewrite Int.testbit_repr; auto. 
+  intros. unfold loword. rewrite Int.testbit_repr; auto.
 Qed.
 
 Lemma bits_hiword:
@@ -3937,7 +3937,7 @@ Proof.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   fold (testbit (shru n (repr Int.zwordsize)) i). rewrite bits_shru.
   change (unsigned (repr Int.zwordsize)) with Int.zwordsize.
-  apply zlt_true. omega. omega. 
+  apply zlt_true. omega. omega.
 Qed.
 
 Lemma bits_ofwords:
@@ -3945,53 +3945,53 @@ Lemma bits_ofwords:
   testbit (ofwords hi lo) i =
   if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize).
 Proof.
-  intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto. 
-  change (unsigned (repr Int.zwordsize)) with Int.zwordsize. 
+  intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto.
+  change (unsigned (repr Int.zwordsize)) with Int.zwordsize.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   destruct (zlt i Int.zwordsize).
-  rewrite testbit_repr; auto. 
+  rewrite testbit_repr; auto.
   rewrite !testbit_repr; auto.
-  fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. 
+  fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto.
   omega.
 Qed.
 
 Lemma lo_ofwords:
   forall hi lo, loword (ofwords hi lo) = lo.
 Proof.
-  intros. apply Int.same_bits_eq; intros. 
-  rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. omega. 
+  intros. apply Int.same_bits_eq; intros.
+  rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. omega.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
 Qed.
 
 Lemma hi_ofwords:
   forall hi lo, hiword (ofwords hi lo) = hi.
 Proof.
-  intros. apply Int.same_bits_eq; intros. 
+  intros. apply Int.same_bits_eq; intros.
   rewrite bits_hiword; auto. rewrite bits_ofwords.
-  rewrite zlt_false. f_equal. omega. omega. 
+  rewrite zlt_false. f_equal. omega. omega.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
 Qed.
 
 Lemma ofwords_recompose:
   forall n, ofwords (hiword n) (loword n) = n.
 Proof.
-  intros. apply same_bits_eq; intros. rewrite bits_ofwords; auto. 
-  destruct (zlt i Int.zwordsize). 
-  apply bits_loword. omega. 
-  rewrite bits_hiword. f_equal. omega. 
+  intros. apply same_bits_eq; intros. rewrite bits_ofwords; auto.
+  destruct (zlt i Int.zwordsize).
+  apply bits_loword. omega.
+  rewrite bits_hiword. f_equal. omega.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega.
 Qed.
 
 Lemma ofwords_add:
   forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo).
 Proof.
-  intros. unfold ofwords. rewrite shifted_or_is_add. 
-  apply eqm_samerepr. apply eqm_add. apply eqm_mult. 
+  intros. unfold ofwords. rewrite shifted_or_is_add.
+  apply eqm_samerepr. apply eqm_add. apply eqm_mult.
   apply eqm_sym; apply eqm_unsigned_repr.
-  apply eqm_refl. 
+  apply eqm_refl.
   apply eqm_sym; apply eqm_unsigned_repr.
   change Int.zwordsize with 32; change zwordsize with 64; omega.
-  rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B. 
+  rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B.
   assert (Int.max_unsigned < max_unsigned) by (compute; auto).
   generalize (Int.unsigned_range_2 lo); omega.
 Qed.
@@ -4000,7 +4000,7 @@ Lemma ofwords_add':
   forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo.
 Proof.
   intros. rewrite ofwords_add. apply unsigned_repr.
-  generalize (Int.unsigned_range hi) (Int.unsigned_range lo). 
+  generalize (Int.unsigned_range hi) (Int.unsigned_range lo).
   change (two_p 32) with Int.modulus.
   change Int.modulus with 4294967296.
   change max_unsigned with 18446744073709551615.
@@ -4011,7 +4011,7 @@ Remark eqm_mul_2p32:
   forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32).
 Proof.
   intros. destruct H as [k EQ]. exists k. rewrite EQ.
-  change Int.modulus with (two_p 32). 
+  change Int.modulus with (two_p 32).
   change modulus with (two_p 32 * two_p 32).
   ring.
 Qed.
@@ -4023,7 +4023,7 @@ Proof.
   replace (repr (Int.unsigned hi * two_p 32 + Int.unsigned lo))
      with (repr (Int.signed hi * two_p 32 + Int.unsigned lo)).
   apply signed_repr.
-  generalize (Int.signed_range hi) (Int.unsigned_range lo). 
+  generalize (Int.signed_range hi) (Int.unsigned_range lo).
   change (two_p 32) with Int.modulus.
   change min_signed with (Int.min_signed * Int.modulus).
   change max_signed with (Int.max_signed * Int.modulus + Int.modulus - 1).
@@ -4074,7 +4074,7 @@ Lemma decompose_not:
   forall xh xl,
   not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl).
 Proof.
-  intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal. 
+  intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal.
   apply (Int64.eq_spec mone (ofwords Int.mone Int.mone)).
 Qed.
 
@@ -4087,21 +4087,21 @@ Lemma decompose_shl_1:
 Proof.
   intros.
   assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   apply Int64.same_bits_eq; intros.
   rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto.
-  destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega. 
-  destruct (zlt i (Int.unsigned y)). auto. 
+  destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega.
+  destruct (zlt i (Int.unsigned y)). auto.
   rewrite bits_ofwords by omega. rewrite zlt_true by omega. auto.
-  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
-  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega.
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega.
   rewrite Int.bits_shru by omega. rewrite H0.
   destruct (zlt (i - Int.unsigned y) (Int.zwordsize)).
   rewrite zlt_true by omega. rewrite zlt_true by omega.
-  rewrite orb_false_l. f_equal. omega. 
-  rewrite zlt_false by omega. rewrite zlt_false by omega. 
+  rewrite orb_false_l. f_equal. omega.
+  rewrite zlt_false by omega. rewrite zlt_false by omega.
   rewrite orb_false_r. f_equal. omega.
 Qed.
 
@@ -4114,16 +4114,16 @@ Proof.
   intros.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
   apply Int64.same_bits_eq; intros.
   rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto.
   destruct (zlt i Int.zwordsize). rewrite zlt_true by omega. apply Int.bits_zero.
-  rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_shl by omega.
   destruct (zlt i (Int.unsigned y)).
-  rewrite zlt_true by omega. auto. 
-  rewrite zlt_false by omega. 
-  rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega. 
+  rewrite zlt_true by omega. auto.
+  rewrite zlt_false by omega.
+  rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega.
 Qed.
 
 Lemma decompose_shru_1:
@@ -4135,25 +4135,25 @@ Lemma decompose_shru_1:
 Proof.
   intros.
   assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   apply Int64.same_bits_eq; intros.
   rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto.
   destruct (zlt i Int.zwordsize).
-  rewrite zlt_true by omega. 
+  rewrite zlt_true by omega.
   rewrite bits_ofwords by omega.
-  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega.
   rewrite Int.bits_shru by omega. rewrite H0.
   destruct (zlt (i + Int.unsigned y) (Int.zwordsize)).
   rewrite zlt_true by omega.
   rewrite orb_false_r. auto.
-  rewrite zlt_false by omega. 
+  rewrite zlt_false by omega.
   rewrite orb_false_l. f_equal. omega.
-  rewrite Int.bits_shru by omega. 
+  rewrite Int.bits_shru by omega.
   destruct (zlt (i + Int.unsigned y) zwordsize).
-  rewrite bits_ofwords by omega. 
-  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. 
+  rewrite bits_ofwords by omega.
+  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega.
   rewrite zlt_false by omega. auto.
 Qed.
 
@@ -4166,15 +4166,15 @@ Proof.
   intros.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
   apply Int64.same_bits_eq; intros.
   rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto.
   destruct (zlt i Int.zwordsize).
   rewrite Int.bits_shru by omega. rewrite H1.
   destruct (zlt (i + Int.unsigned y) zwordsize).
-  rewrite zlt_true by omega. rewrite bits_ofwords by omega. 
-  rewrite zlt_false by omega. f_equal; omega. 
+  rewrite zlt_true by omega. rewrite bits_ofwords by omega.
+  rewrite zlt_false by omega. f_equal; omega.
   rewrite zlt_false by omega. auto.
   rewrite zlt_false by omega. apply Int.bits_zero.
 Qed.
@@ -4188,26 +4188,26 @@ Lemma decompose_shr_1:
 Proof.
   intros.
   assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. }
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   apply Int64.same_bits_eq; intros.
   rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto.
   destruct (zlt i Int.zwordsize).
-  rewrite zlt_true by omega. 
+  rewrite zlt_true by omega.
   rewrite bits_ofwords by omega.
-  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. 
+  rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega.
   rewrite Int.bits_shru by omega. rewrite H0.
   destruct (zlt (i + Int.unsigned y) (Int.zwordsize)).
   rewrite zlt_true by omega.
   rewrite orb_false_r. auto.
-  rewrite zlt_false by omega. 
+  rewrite zlt_false by omega.
   rewrite orb_false_l. f_equal. omega.
-  rewrite Int.bits_shr by omega. 
+  rewrite Int.bits_shr by omega.
   destruct (zlt (i + Int.unsigned y) zwordsize).
-  rewrite bits_ofwords by omega. 
-  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. 
-  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
+  rewrite bits_ofwords by omega.
+  rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega.
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega.
   rewrite zlt_false by omega. f_equal.
 Qed.
 
@@ -4221,24 +4221,24 @@ Proof.
   intros.
   assert (zwordsize = 2 * Int.zwordsize) by reflexivity.
   assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize).
-  { unfold Int.sub. rewrite Int.unsigned_repr. auto. 
+  { unfold Int.sub. rewrite Int.unsigned_repr. auto.
     rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. }
   apply Int64.same_bits_eq; intros.
   rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto.
   destruct (zlt i Int.zwordsize).
   rewrite Int.bits_shr by omega. rewrite H1.
   destruct (zlt (i + Int.unsigned y) zwordsize).
-  rewrite zlt_true by omega. rewrite bits_ofwords by omega. 
-  rewrite zlt_false by omega. f_equal; omega. 
-  rewrite zlt_false by omega. rewrite bits_ofwords by omega. 
+  rewrite zlt_true by omega. rewrite bits_ofwords by omega.
+  rewrite zlt_false by omega. f_equal; omega.
+  rewrite zlt_false by omega. rewrite bits_ofwords by omega.
   rewrite zlt_false by omega. auto.
-  rewrite Int.bits_shr by omega. 
+  rewrite Int.bits_shr by omega.
   change (Int.unsigned (Int.sub Int.iwordsize Int.one)) with (Int.zwordsize - 1).
   destruct (zlt (i + Int.unsigned y) zwordsize);
   rewrite bits_ofwords by omega.
-  symmetry. rewrite zlt_false by omega. f_equal. 
+  symmetry. rewrite zlt_false by omega. f_equal.
   destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
-  symmetry. rewrite zlt_false by omega. f_equal. 
+  symmetry. rewrite zlt_false by omega. f_equal.
   destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
 Qed.
 
@@ -4249,8 +4249,8 @@ Lemma decompose_add:
           (Int.add xl yl).
 Proof.
   intros. symmetry. rewrite ofwords_add. rewrite add_unsigned.
-  apply eqm_samerepr. 
-  rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl). 
+  apply eqm_samerepr.
+  rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl).
   set (cc := Int.add_carry xl yl Int.zero).
   set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh);
   set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh).
@@ -4264,8 +4264,8 @@ Proof.
   apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32.
   replace (Xh + Yh) with ((Xh + Yh + Int.unsigned cc) - Int.unsigned cc) by ring.
   apply Int.eqm_sub. 2: apply Int.eqm_refl.
-  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. 
-  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl.
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
 Qed.
 
 Lemma decompose_sub:
@@ -4275,8 +4275,8 @@ Lemma decompose_sub:
           (Int.sub xl yl).
 Proof.
   intros. symmetry. rewrite ofwords_add.
-  apply eqm_samerepr. 
-  rewrite ! ofwords_add'. rewrite (Int.unsigned_sub_borrow xl yl). 
+  apply eqm_samerepr.
+  rewrite ! ofwords_add'. rewrite (Int.unsigned_sub_borrow xl yl).
   set (bb := Int.sub_borrow xl yl Int.zero).
   set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh);
   set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh).
@@ -4290,8 +4290,8 @@ Proof.
   apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32.
   replace (Xh - Yh) with ((Xh - Yh - Int.unsigned bb) + Int.unsigned bb) by ring.
   apply Int.eqm_add. 2: apply Int.eqm_refl.
-  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. 
-  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl.
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
 Qed.
 
 Lemma decompose_sub':
@@ -4300,9 +4300,9 @@ Lemma decompose_sub':
   ofwords (Int.add (Int.add xh (Int.not yh)) (Int.add_carry xl (Int.not yl) Int.one))
           (Int.sub xl yl).
 Proof.
-  intros. rewrite decompose_sub. f_equal. 
+  intros. rewrite decompose_sub. f_equal.
   rewrite Int.sub_borrow_add_carry by auto.
-  rewrite Int.sub_add_not_3. rewrite Int.xor_assoc. rewrite Int.xor_idem. 
+  rewrite Int.sub_add_not_3. rewrite Int.xor_assoc. rewrite Int.xor_idem.
   rewrite Int.xor_zero. auto.
   rewrite Int.xor_zero_l. unfold Int.add_carry.
   destruct (zlt (Int.unsigned xl + Int.unsigned (Int.not yl) + Int.unsigned Int.one) Int.modulus);
@@ -4314,12 +4314,12 @@ Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
 Lemma mul'_mulhu:
   forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y).
 Proof.
-  intros. 
-  rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. 
+  intros.
+  rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul.
   set (p := Int.unsigned x * Int.unsigned y).
-  set (ph := p / Int.modulus). set (pl := p mod Int.modulus). 
+  set (ph := p / Int.modulus). set (pl := p mod Int.modulus).
   transitivity (repr (ph * Int.modulus + pl)).
-- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. 
+- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos.
 - apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints.
   rewrite Int.unsigned_repr_eq. apply eqm_refl.
 Qed.
@@ -4330,7 +4330,7 @@ Lemma decompose_mul:
   ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl))
           (loword (mul' xl yl)).
 Proof.
-  intros. 
+  intros.
   set (pl := loword (mul' xl yl)); set (ph := hiword (mul' xl yl)).
   assert (EQ0: unsigned (mul' xl yl) = Int.unsigned ph * two_p 32 + Int.unsigned pl).
   { rewrite <- (ofwords_recompose (mul' xl yl)). apply ofwords_add'. }
@@ -4339,7 +4339,7 @@ Proof.
   set (YL := Int.unsigned yl); set (YH := Int.unsigned yh).
   set (PH := Int.unsigned ph) in *. set (PL := Int.unsigned pl) in *.
   transitivity (repr (((PH + XL * YH) + XH * YL) * two_p 32 + PL)).
-  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl.
   apply eqm_mul_2p32.
   rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add.
   rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add.
@@ -4349,14 +4349,14 @@ Proof.
   transitivity (repr (unsigned (mul' xl yl) + (XL * YH + XH * YL) * two_p 32)).
   rewrite EQ0. f_equal. ring.
   transitivity (repr ((XL * YL + (XL * YH + XH * YL) * two_p 32))).
-  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl.
   unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl.
   transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
-  rewrite Zplus_0_l; auto. 
+  rewrite Zplus_0_l; auto.
   transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
-  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. 
-  change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. 
-  f_equal. ring. 
+  apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl.
+  change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring.
+  f_equal. ring.
 Qed.
 
 Lemma decompose_mul_2:
@@ -4365,7 +4365,7 @@ Lemma decompose_mul_2:
   ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl))
           (Int.mul xl yl).
 Proof.
-  intros. rewrite decompose_mul. rewrite mul'_mulhu. 
+  intros. rewrite decompose_mul. rewrite mul'_mulhu.
   rewrite hi_ofwords, lo_ofwords. auto.
 Qed.
 
@@ -4375,11 +4375,11 @@ Lemma decompose_ltu:
 Proof.
   intros. unfold ltu. rewrite ! ofwords_add'. unfold Int.ltu, Int.eq.
   destruct (zeq (Int.unsigned xh) (Int.unsigned yh)).
-  rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). 
+  rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)).
   apply zlt_true; omega.
   apply zlt_false; omega.
-  change (two_p 32) with Int.modulus. 
-  generalize (Int.unsigned_range xl) (Int.unsigned_range yl). 
+  change (two_p 32) with Int.modulus.
+  generalize (Int.unsigned_range xl) (Int.unsigned_range yl).
   change Int.modulus with 4294967296. intros.
   destruct (zlt (Int.unsigned xh) (Int.unsigned yh)).
   apply zlt_true; omega.
@@ -4392,9 +4392,9 @@ Lemma decompose_leu:
   if Int.eq xh yh then negb (Int.ltu yl xl) else Int.ltu xh yh.
 Proof.
   intros. rewrite decompose_ltu. rewrite Int.eq_sym.
-  unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). 
+  unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)).
   auto.
-  unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). 
+  unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)).
   rewrite zlt_false by omega; auto.
   rewrite zlt_true by omega; auto.
 Qed.
@@ -4403,13 +4403,13 @@ Lemma decompose_lt:
   forall xh xl yh yl,
   lt (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.lt xh yh.
 Proof.
-  intros. unfold lt. rewrite ! ofwords_add''. rewrite Int.eq_signed. 
+  intros. unfold lt. rewrite ! ofwords_add''. rewrite Int.eq_signed.
   destruct (zeq (Int.signed xh) (Int.signed yh)).
-  rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). 
+  rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)).
   apply zlt_true; omega.
   apply zlt_false; omega.
-  change (two_p 32) with Int.modulus. 
-  generalize (Int.unsigned_range xl) (Int.unsigned_range yl). 
+  change (two_p 32) with Int.modulus.
+  generalize (Int.unsigned_range xl) (Int.unsigned_range yl).
   change Int.modulus with 4294967296. intros.
   unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)).
   apply zlt_true; omega.
@@ -4422,9 +4422,9 @@ Lemma decompose_le:
   if Int.eq xh yh then negb (Int.ltu yl xl) else Int.lt xh yh.
 Proof.
   intros. rewrite decompose_lt. rewrite Int.eq_sym.
-  rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). 
+  rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)).
   auto.
-  unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). 
+  unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)).
   rewrite zlt_false by omega; auto.
   rewrite zlt_true by omega; auto.
 Qed.