lib/Coqlib.v: remove defns about multiplication, division, modulus

Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).

15 files changed, 52 insertions, 135 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 60c214d0..8e1cd367 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -532,7 +532,7 @@ Lemma mk_shift_amount_eq:
   forall n, Int.ltu n Int.iwordsize = true -> s_amount (mk_shift_amount n) = n.
 Proof.
   intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)).
-  decEq. apply Zmod_small. apply Int.ltu_inv; auto.
+  decEq. apply Z.mod_small. apply Int.ltu_inv; auto.
   apply Int.repr_unsigned.
 Qed.
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 2dcb8956..45051bcf 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -755,13 +755,13 @@ Proof.
   assert (2 <= sz -> (2 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). auto.
-    destruct (zle sz 4). apply Zdivides_trans with 4; auto. exists 2; auto.
-    apply Zdivides_trans with 8; auto. exists 4; auto.
+    destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 4; auto.
   assert (4 <= sz -> (4 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
     destruct (zle sz 4). auto.
-    apply Zdivides_trans with 8; auto. exists 2; auto.
+    apply Z.divide_trans with 8; auto. exists 2; auto.
   assert (8 <= sz -> (8 | n)). intros.
     destruct (zle sz 1). omegaContradiction.
     destruct (zle sz 2). omegaContradiction.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index fc163719..55fa7a67 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -39,7 +39,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   | Outgoing => zle 0 ofs
   | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
   end
-  && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
+  && Zdivide_dec (typealign ty) ofs.
 
 Definition slot_writable (sl: slot) : bool :=
   match sl with
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 9e24857a..e660677a 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -57,13 +57,13 @@ Proof.
     apply Z.mul_nonneg_nonneg; omega.
   assert (k * n <= two_p (N + l) - two_p l).
     apply Z.le_trans with (two_p l * n).
-    apply Zmult_le_compat_r. omega. omega.
+    apply Z.mul_le_mono_nonneg_r; omega.
     replace (N + l) with (l + N) by omega.
     rewrite two_p_is_exp.
     replace (two_p l * two_p N - two_p l)
        with (two_p l * (two_p N - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
     omega. omega.
   assert (0 <= two_p (N + l) * r).
     apply Z.mul_nonneg_nonneg.
@@ -72,7 +72,7 @@ Proof.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1)) by ring.
-    apply Zmult_le_compat_l.
+    apply Z.mul_le_mono_nonneg_l. 
     omega.
     exploit (two_p_gt_ZERO (N + l)). omega. omega.
   assert (0 <= m * n - two_p (N + l) * q).
@@ -138,13 +138,13 @@ Proof.
   rewrite H2.
   assert (k * n <= two_p (N + l)).
     rewrite Z.add_comm. rewrite two_p_is_exp; try omega.
-    apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega.
+    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1))
          by ring.
-    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega.
   omega.
 Qed.
 
@@ -246,10 +246,11 @@ Proof.
   unfold Int.max_signed; omega.
   apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos.
   apply Int.modulus_pos.
-  split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int.min_signed * m). 
+  apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto.
   apply Z.le_lt_trans with (Int.half_modulus * m).
-  apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto.
+  apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega.
   apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto.
   assert (32 < Int.max_unsigned) by (compute; auto). omega.
   unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr.
@@ -290,7 +291,7 @@ Proof.
   apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned.
   apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2.
   apply (f_equal (fun x => n * x / Int.modulus)).
-  rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
@@ -400,8 +401,9 @@ Proof.
   unfold Int64.max_signed; omega.
   apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
   apply Int64.modulus_pos.
-  split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
-  apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto.
+  split. apply Z.le_trans with (Int64.min_signed * m).
+  apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto.
   apply Z.le_lt_trans with (Int64.half_modulus * m).
   apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
   apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
@@ -444,7 +446,7 @@ Proof.
   apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned.
   apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2.
   apply (f_equal (fun x => n * x / Int64.modulus)).
-  rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption.
+  rewrite Int64.signed_repr_eq. rewrite Z.mod_small by assumption.
   apply zlt_false. assumption.
 Qed.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index afc470b3..621459d0 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -506,7 +506,7 @@ Proof.
   unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal.
   apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
 - intros until i0; intros EVAL R. exists v; split; auto.
-  inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor.
+  inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor.
 - constructor.
 - apply Int.unsigned_range.
 Qed.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 37a9ecf2..47b87bfb 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1492,12 +1492,12 @@ Proof.
   inv H; auto with va.
 - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
   generalize (Int.unsigned_range n); intros.
-  rewrite Zmod_small by omega.
+  rewrite Z.mod_small by omega.
   apply H1. omega. omega.
 - destruct (zlt n0 Int.zwordsize); auto with va.
   apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
   generalize (Int.unsigned_range n); intros.
-  rewrite ! Zmod_small by omega.
+  rewrite ! Z.mod_small by omega.
   rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
 - destruct (zlt n0 Int.zwordsize); auto with va.
 Qed.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 823d2542..7f5fe355 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -292,7 +292,6 @@ Remark check_assign_copy:
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
 Proof with try (right; intuition omega).
   intros. unfold assign_copy_ok.
-  assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto...
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto...
   assert (Y: {b' <> b \/
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ffafc5d2..5acb996d 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -923,7 +923,7 @@ Remark inj_offset_aligned_block:
   Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz.
 Proof.
   intros; red; intros.
-  apply Zdivides_trans with (block_alignment sz).
+  apply Z.divide_trans with (block_alignment sz).
   unfold align_chunk.  unfold block_alignment.
   generalize Z.divide_1_l; intro.
   generalize Z.divide_refl; intro.
diff --git a/common/Memdata.v b/common/Memdata.v
index 307a02db..c53f0e5d 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -258,14 +258,14 @@ Lemma decode_encode_int_4:
   forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)).
-  decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
 Qed.
 
 Lemma decode_encode_int_8:
   forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)).
-  decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
 Qed.
 
 (** A length-[n] encoding depends only on the low [8*n] bits of the integer. *)
diff --git a/common/Memory.v b/common/Memory.v
index fed6c1d7..b68a5049 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -284,7 +284,7 @@ Lemma valid_access_dec:
 Proof.
   intros.
   destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
-  destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
+  destruct (Zdivide_dec (align_chunk chunk) ofs).
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
   right; red; intro V; inv V; contradiction.
@@ -887,11 +887,11 @@ Proof.
   intros (bytes1 & bytes2 & LB1 & LB2 & APP).
   change 4 with (size_chunk Mint32) in LB1.
   exploit loadbytes_load. eexact LB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   intros L1.
   change 4 with (size_chunk Mint32) in LB2.
   exploit loadbytes_load. eexact LB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
   exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
   exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
@@ -1644,9 +1644,9 @@ Proof.
   rewrite encode_val_length in SB2. simpl in SB2.
   exists m1; split.
   apply storebytes_store. exact SB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   apply storebytes_store. exact SB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
 Qed.
 
 Theorem storev_int64_split:
diff --git a/common/Separation.v b/common/Separation.v
index a9642d72..1493b535 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -702,7 +702,7 @@ Proof.
 - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega.
 - intros. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto. xomega.
-- red; intros. apply Zdivides_trans with 8; auto.
+- red; intros. apply Z.divide_trans with 8; auto.
   exists (8 / align_chunk chunk). destruct chunk; reflexivity.
 - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
 - intros (j' & INJ' & J1 & J2 & J3).
diff --git a/common/Switch.v b/common/Switch.v
index 0ef91d60..5a6d4c63 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -288,10 +288,10 @@ Lemma validate_jumptable_correct:
 Proof.
   intros.
   rewrite (validate_jumptable_correct_rec cases tbl ofs); auto.
-- f_equal. f_equal. rewrite Zmod_small. omega.
+- f_equal. f_equal. rewrite Z.mod_small. omega.
   destruct (zle ofs v). omega.
   assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus).
-  { rewrite Zmod_small. omega. omega. }
+  { rewrite Z.mod_small. omega. omega. }
   rewrite Z_mod_plus in M by auto. rewrite M in H0. omega.
 - generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega.
 Qed.
@@ -331,7 +331,7 @@ Proof.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
   assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega).
   destruct (zlt ((v - ofs) mod modulus) sz).
-  rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto.
+  rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto.
   eapply IHt; eauto.
 Qed.
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 90e0b89d..02c5d07f 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -411,42 +411,12 @@ Qed.
 
 (** Properties of Euclidean division and modulus. *)
 
-Lemma Zdiv_small:
-  forall x y, 0 <= x < y -> x / y = 0.
-Proof.
-  intros. assert (y > 0). omega.
-  assert (forall a b,
-    0 <= a < y ->
-    0 <= y * b + a < y ->
-    b = 0).
-  intros.
-  assert (b = 0 \/ b > 0 \/ (-b) > 0). omega.
-  elim H3; intro.
-  auto.
-  elim H4; intro.
-  assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega.
-  omegaContradiction.
-  assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega.
-  rewrite <- Zopp_mult_distr_r in H6. omegaContradiction.
-  apply H1 with (x mod y).
-  apply Z_mod_lt. auto.
-  rewrite <- Z_div_mod_eq. auto. auto.
-Qed.
-
-Lemma Zmod_small:
-  forall x y, 0 <= x < y -> x mod y = x.
-Proof.
-  intros. assert (y > 0). omega.
-  generalize (Z_div_mod_eq x y H0).
-  rewrite (Zdiv_small x y H). omega.
-Qed.
-
 Lemma Zmod_unique:
   forall x y a b,
   x = a * y + b -> 0 <= b < y -> x mod y = b.
 Proof.
   intros. subst x. rewrite Z.add_comm.
-  rewrite Z_mod_plus. apply Zmod_small. auto. omega.
+  rewrite Z_mod_plus. apply Z.mod_small. auto. omega.
 Qed.
 
 Lemma Zdiv_unique:
@@ -461,30 +431,7 @@ Lemma Zdiv_Zdiv:
   forall a b c,
   b > 0 -> c > 0 -> (a / b) / c = a / (b * c).
 Proof.
-  intros.
-  generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros.
-  generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros.
-  set (q1 := a / b) in *. set (r1 := a mod b) in *.
-  set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *.
-  symmetry. apply Zdiv_unique with (r2 * b + r1).
-  rewrite H2. rewrite H4. ring.
-  split.
-  assert (0 <= r2 * b). apply Z.mul_nonneg_nonneg. omega. omega. omega.
-  assert ((r2 + 1) * b <= c * b).
-  apply Zmult_le_compat_r. omega. omega.
-  replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring.
-  replace (c * b) with (b * c) in H5 by ring.
-  omega.
-Qed.
-
-Lemma Zmult_le_compat_l_neg :
-  forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.
-Proof.
-  intros.
-  assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega.
-  replace (p * n) with (- ((-p) * n)) by ring.
-  replace (p * m) with (- ((-p) * m)) by ring.
-  omega.
+  intros. apply Z.div_div; omega.
 Qed.
 
 Lemma Zdiv_interval_1:
@@ -516,9 +463,9 @@ Proof.
   intros.
   assert (lo <= a / b < hi+1).
   apply Zdiv_interval_1. omega. omega. auto.
-  assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega.
+  assert (lo * b <= lo * 1) by (apply Z.mul_le_mono_nonpos_l; omega).
   replace (lo * 1) with lo in H3 by ring.
-  assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega.
+  assert ((hi + 1) * 1 <= (hi + 1) * b) by (apply Z.mul_le_mono_nonneg_l; omega).
   replace ((hi + 1) * 1) with (hi + 1) in H4 by ring.
   omega.
   omega.
@@ -529,42 +476,11 @@ Lemma Zmod_recombine:
   a > 0 -> b > 0 ->
   x mod (a * b) = ((x/b) mod a) * b + (x mod b).
 Proof.
-  intros.
-  set (xb := x/b).
-  apply Zmod_unique with (xb/a).
-  generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1.
-  generalize (Z_div_mod_eq xb a H); intro EQ2.
-  rewrite EQ2 in EQ1.
-  eapply eq_trans. eexact EQ1. ring.
-  generalize (Z_mod_lt x b H0). intro.
-  generalize (Z_mod_lt xb a H). intro.
-  assert (0 <= xb mod a * b <= a * b - b).
-    split. apply Z.mul_nonneg_nonneg; omega.
-    replace (a * b - b) with ((a - 1) * b) by ring.
-    apply Zmult_le_compat; omega.
-  omega.
+  intros. rewrite (Z.mul_comm a b). rewrite Z.rem_mul_r by omega. ring. 
 Qed.
 
 (** Properties of divisibility. *)
 
-Lemma Zdivides_trans:
-  forall x y z, (x | y) -> (y | z) -> (x | z).
-Proof.
-  intros x y z [a A] [b B]; subst. exists (a*b); ring.
-Qed.
-
-Definition Zdivide_dec:
-  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
-Proof.
-  intros. destruct (zeq (Z.modulo q p) 0).
-  left. exists (q / p).
-  transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto.
-  transitivity (p * (q / p)). omega. ring.
-  right; red; intros. elim n. apply Z_div_exact_1; auto.
-  inv H0. rewrite Z_div_mult; auto. ring.
-Defined.
-Global Opaque Zdivide_dec.
-
 Lemma Zdivide_interval:
   forall a b c,
   0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c.
diff --git a/lib/Floats.v b/lib/Floats.v
index 3ce8f4b4..f93505fc 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -1218,7 +1218,7 @@ Proof.
   set (m := n mod 2^p + (2^p-1)) in *.
   assert (C: m / 2^p = if zeq (n mod 2^p) 0 then 0 else 1).
   { unfold m. destruct (zeq (n mod 2^p) 0).
-    rewrite e. apply Zdiv_small. omega.
+    rewrite e. apply Z.div_small. omega.
     eapply Zdiv_unique with (n mod 2^p - 1). ring. omega. }
   assert (D: Z.testbit m p = if zeq (n mod 2^p) 0 then false else true).
   { destruct (zeq (n mod 2^p) 0).
@@ -1226,7 +1226,7 @@ Proof.
     apply Z.testbit_true; auto. rewrite C; auto. }
   assert (E: forall i, p < i -> Z.testbit m i = false).
   { intros. apply Z.testbit_false. omega.
-    replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small.
+    replace (m / 2^i) with 0. auto. symmetry. apply Z.div_small.
     unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega.
     change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega.
     apply Zpower_le. omega. }
diff --git a/lib/Integers.v b/lib/Integers.v
index 4b75e71e..64263b97 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -539,7 +539,7 @@ Lemma eqmod_small_eq:
 Proof.
   intros x y [k EQ] I1 I2.
   generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
-  rewrite (Zdiv_small x modul I1) in H. subst k. omega.
+  rewrite (Z.div_small x modul I1) in H. subst k. omega.
 Qed.
 
 Lemma eqmod_mod_eq:
@@ -712,7 +712,7 @@ Theorem repr_unsigned:
   forall i, repr (unsigned i) = i.
 Proof.
   destruct i; simpl. unfold repr. apply mkint_eq.
-  rewrite Z_mod_modulus_eq. apply Zmod_small; omega.
+  rewrite Z_mod_modulus_eq. apply Z.mod_small; omega.
 Qed.
 Hint Resolve repr_unsigned: ints.
 
@@ -735,7 +735,7 @@ Theorem unsigned_repr:
   forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
 Proof.
   intros. rewrite unsigned_repr_eq.
-  apply Zmod_small. unfold max_unsigned in H. omega.
+  apply Z.mod_small. unfold max_unsigned in H. omega.
 Qed.
 Hint Resolve unsigned_repr: ints.
 
@@ -782,7 +782,7 @@ Qed.
 
 Theorem unsigned_one: unsigned one = 1.
 Proof.
-  unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega.
+  unfold one; rewrite unsigned_repr_eq. apply Z.mod_small. split. omega.
   unfold modulus. replace wordsize with (S(Init.Nat.pred wordsize)).
   rewrite two_power_nat_S. generalize (two_power_nat_pos (Init.Nat.pred wordsize)).
   omega.
@@ -793,7 +793,7 @@ Theorem unsigned_mone: unsigned mone = modulus - 1.
 Proof.
   unfold mone; rewrite unsigned_repr_eq.
   replace (-1) with ((modulus - 1) + (-1) * modulus).
-  rewrite Z_mod_plus_full. apply Zmod_small.
+  rewrite Z_mod_plus_full. apply Z.mod_small.
   generalize modulus_pos. omega. omega.
 Qed.
 
@@ -825,7 +825,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 Z.mod_small.
   generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
 Qed.
 
@@ -2464,7 +2464,7 @@ Proof.
   - rewrite andb_false_r; auto.
   - generalize (unsigned_range n); intros.
     rewrite bits_mone. rewrite andb_true_r. f_equal.
-    symmetry. apply Zmod_small. omega.
+    symmetry. apply Z.mod_small. omega.
     omega.
 Qed.
 
@@ -2491,7 +2491,7 @@ Theorem rol_zero:
   rol x zero = x.
 Proof.
   bit_solve. f_equal. rewrite unsigned_zero. rewrite Z.sub_0_r.
-  apply Zmod_small; auto.
+  apply Z.mod_small; auto.
 Qed.
 
 Lemma bitwise_binop_rol:
@@ -2616,14 +2616,14 @@ Proof.
   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.
+    rewrite Z.mod_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.
+    apply Z.mod_small; auto.
 Qed.
 
 (** ** Properties of [Z_one_bits] and [is_power2]. *)