Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv

Some details: 

 - ZAux.v is the only file left in Ints/Z. The few elements that remain in it
   are rather specific or compatibility oriented. Others parts and files have 
   been either deleted when unused or pushed into some place of ZArith. 
 - Ints/List/ is removed since it was not needed anymore
 - Ints/Tactic.v disappear: some of its tactic were unused, some already in 
   Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict 
   has been added to Tactics.v
 - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
 - A new file Zpow_facts inherits lots of results about Zpower. Placing them 
   into Zpower would have been difficult with respect to compatibility 
   (import of ring)
 - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
 - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) 
 
Now, concerning Zdiv, the behavior when dividing by a negative number is now 
fully proved. When this was possible, existing lemmas has been extended, 
either from strictly positive to non-zero divisor, or even to arbitrary 
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained 
for compatibility. Several lemmas now have shorter proofs (based on unicity 
lemmas). Lemmas are now more or less organized by themes (division and order, 
division and usual operations, etc). Three possible choices of spec for 
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp 
with the current choice of Zdiv/Zmod is now fully covered. A embryo of 
division "a la Ocaml" is given: Odiv and Omod. 




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

17 files changed, 157 insertions, 179 deletions

diff --git a/theories/Ints/num/GenAdd.v b/theories/Ints/num/GenAdd.v
index 9d4c579020..77f5e23016 100644
--- a/theories/Ints/num/GenAdd.v
+++ b/theories/Ints/num/GenAdd.v
@@ -10,7 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -265,11 +264,11 @@ Section GenAdd.
   Lemma spec_ww_succ : forall x, [[ww_succ x]] = ([[x]] + 1) mod wwB.
   Proof.
    destruct x as [ |xh xl];simpl.
-   rewrite spec_ww_1;rewrite Zmod_def_small;trivial.
+   rewrite spec_ww_1;rewrite Zmod_small;trivial.
    split;[intro;discriminate|apply wwB_pos].
    rewrite <- Zplus_assoc;generalize (spec_w_succ_c xl);
    destruct (w_succ_c xl) as[l|l];intro H;unfold interp_carry in H;rewrite <-H.
-   rewrite Zmod_def_small;trivial.
+   rewrite Zmod_small;trivial.
    rewrite wwB_wBwB;apply beta_mult;apply spec_to_Z.
    assert ([|l|] = 0). clear spec_ww_1 spec_w_1 spec_w_0.
     assert (H1:= spec_to_Z l); assert (H2:= spec_to_Z xl); omega.
@@ -281,10 +280,10 @@ Section GenAdd.
   Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
   Proof.
    destruct x as [ |xh xl];intros y;simpl.
-   rewrite Zmod_def_small;trivial. apply spec_ww_to_Z;trivial.
+   rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial.
    destruct y as [ |yh yl].
    change [[W0]] with 0;rewrite Zplus_0_r.
-   rewrite Zmod_def_small;trivial. 
+   rewrite Zmod_small;trivial. 
     exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)).
    simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) 
    with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring.
diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v
index 6b6376b690..a9936f1dd0 100644
--- a/theories/Ints/num/GenBase.v
+++ b/theories/Ints/num/GenBase.v
@@ -10,8 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
 Require Import Basic_type.
 Require Import JMeq.
 
@@ -188,7 +186,7 @@ Section GenBase.
 
   Lemma lt_0_wB : 0 < wB.
   Proof. 
-   unfold base;apply Zpower_lt_0. unfold Zlt;reflexivity.
+   unfold base;apply Zpower_gt_0. unfold Zlt;reflexivity.
    unfold Zle;intros H;discriminate H.
   Qed.
 
@@ -208,7 +206,7 @@ Section GenBase.
   Proof.
    assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Zmult_1_r 1).
    rewrite Zpower_2.
-   apply Zmult_lt_compat;(split;[unfold Zlt;reflexivity|trivial]).
+   apply Zmult_lt_compat2;(split;[unfold Zlt;reflexivity|trivial]).
    apply Zlt_le_weak;trivial. 
   Qed.
 
@@ -217,11 +215,11 @@ Section GenBase.
    clear spec_w_0 w_0 spec_w_1 w_1 spec_w_Bm1 w_Bm1 spec_w_WW spec_w_0W 
     spec_to_Z;unfold base.
    assert (2 ^ Zpos w_digits = 2 * (2 ^ (Zpos w_digits - 1))).
-   pattern 2 at 2; rewrite <- Zpower_exp_1.
+   pattern 2 at 2; rewrite <- Zpower_1_r.
    rewrite <- Zpower_exp; auto with zarith.
-   eq_tac; auto with zarith.
+   f_equal; auto with zarith.
    case w_digits; compute; intros; discriminate.
-   rewrite H; eq_tac; auto with zarith.
+   rewrite H; f_equal; auto with zarith.
    rewrite Zmult_comm; apply Z_div_mult; auto with zarith.
   Qed.
 
@@ -239,17 +237,17 @@ Section GenBase.
    (z*wB + [|x|]) mod wwB = (z mod wB)*wB + [|x|].
   Proof.
    intros z x.
-   rewrite Zmod_plus. 2:apply lt_0_wwB.
+   rewrite Zplus_mod. 
    pattern wwB at 1;rewrite wwB_wBwB; rewrite Zpower_2.
    rewrite Zmult_mod_distr_r;try apply lt_0_wB.
-   rewrite (Zmod_def_small [|x|]).
-   apply Zmod_def_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z.
+   rewrite (Zmod_small [|x|]).
+   apply Zmod_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z.
    apply Z_mod_lt;apply Zlt_gt;apply lt_0_wB.
    destruct (spec_to_Z x);split;trivial.
    change [|x|] with (0*wB+[|x|]). rewrite wwB_wBwB.
    rewrite Zpower_2;rewrite <- (Zplus_0_r (wB*wB));apply beta_lex_inv.
    apply lt_0_wB. apply spec_to_Z. split;[apply Zle_refl | apply lt_0_wB].
-  Qed.
+ Qed.
 
   Lemma wB_div : forall x y, ([|x|] * wB + [|y|]) / wB = [|x|].
   Proof.
@@ -321,7 +319,7 @@ Section GenBase.
   apply Zmult_le_compat; auto with zarith.
   apply Zle_trans with wB; auto with zarith.
   unfold base.
-  rewrite <- (ZAux.Zpower_exp_0 2).
+  rewrite <- (Zpower_0_r 2).
   apply Zpower_le_monotone2; auto with zarith.
   unfold base; auto with zarith.
   Qed.
diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v
index 6466c198ff..237adb48b0 100644
--- a/theories/Ints/num/GenDiv.v
+++ b/theories/Ints/num/GenDiv.v
@@ -10,8 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenDivn1.
@@ -102,42 +100,41 @@ Section POS_MOD.
  assert (F0: forall x y, x - y + y = x); auto with zarith.
  intros w1 p; case (spec_to_w_Z p); intros HH1 HH2.
  unfold ww_pos_mod; case w1.
- simpl; rewrite Zmod_def_small; split; auto with zarith.
+ simpl; rewrite Zmod_small; split; auto with zarith.
  intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits));
     case ww_compare; 
     rewrite spec_w_0W; rewrite spec_zdigits; fold wB;
     intros H1.
    rewrite H1; simpl ww_to_Z.
    autorewrite with w_rewrite rm10.
-   rewrite Zmod_plus; auto with zarith.
-   rewrite Zmod_mult_0; auto with zarith.
+   rewrite Zplus_mod; auto with zarith.
+   rewrite Z_mod_mult; auto with zarith.
    autorewrite with rm10.
    rewrite Zmod_mod; auto with zarith.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    autorewrite with w_rewrite rm10.
    simpl ww_to_Z.
    rewrite spec_pos_mod.
    assert (HH0: [|low p|] = [[p]]).
      rewrite spec_low.
-     apply Zmod_def_small; auto with zarith.
+     apply Zmod_small; auto with zarith.
      case (spec_to_w_Z p); intros HHH1 HHH2; split; auto with zarith.
      apply Zlt_le_trans with (1 := H1).
-     unfold base.
-     apply Zpower2_le_lin; auto with zarith.
+     unfold base; apply Zpower2_le_lin; auto with zarith.
    rewrite HH0.
-   rewrite Zmod_plus; auto with zarith.
+   rewrite Zplus_mod; auto with zarith.
    unfold base.
    rewrite <- (F0 (Zpos w_digits) [[p]]).
    rewrite Zpower_exp; auto with zarith.
    rewrite Zmult_assoc.
-   rewrite Zmod_mult_0; auto with zarith.
+   rewrite Z_mod_mult; auto with zarith.
    autorewrite with w_rewrite rm10.
    rewrite Zmod_mod; auto with zarith.
 generalize (spec_ww_compare p ww_zdigits);
     case ww_compare; rewrite spec_ww_zdigits; 
                      rewrite spec_zdigits; intros H2.
   replace (2^[[p]]) with wwB.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
   unfold base; rewrite H2.
   rewrite spec_ww_digits; auto.
   assert (HH0: [|low (ww_sub p (w_0W w_zdigits))|] = 
@@ -146,7 +143,7 @@ generalize (spec_ww_compare p ww_zdigits);
     rewrite spec_ww_sub.
     rewrite spec_w_0W; rewrite spec_zdigits.
     rewrite <- Zmod_div_mod; auto with zarith.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
     split; auto with zarith.
     apply Zlt_le_trans with (Zpos w_digits); auto with zarith.
     unfold base; apply Zpower2_le_lin; auto with zarith.
@@ -162,11 +159,11 @@ generalize (spec_ww_compare p ww_zdigits);
    unfold base; rewrite <- Zmult_assoc; rewrite <- Zpower_exp;
     auto with zarith.
    rewrite F0; auto with zarith.
-   rewrite <- Zplus_assoc; rewrite Zmod_plus; auto with zarith.
-   rewrite Zmod_mult_0; auto with zarith.
+   rewrite <- Zplus_assoc; rewrite Zplus_mod; auto with zarith.
+   rewrite Z_mod_mult; auto with zarith.
    autorewrite with rm10.
    rewrite Zmod_mod; auto with zarith.
-   apply sym_equal; apply Zmod_def_small; auto with zarith.
+   apply sym_equal; apply Zmod_small; auto with zarith.
    case (spec_to_Z xh); intros U1 U2.
    case (spec_to_Z xl); intros U3 U4.
    split; auto with zarith.
@@ -186,7 +183,7 @@ generalize (spec_ww_compare p ww_zdigits);
    case (spec_to_Z xl); unfold base; auto with zarith.
    rewrite Zmult_minus_distr_r; rewrite <- Zpower_exp; auto with zarith.
    rewrite F0; auto with zarith.
-  rewrite Zmod_def_small; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
   case (spec_to_w_Z (WW xh xl)); intros U1 U2.
   split; auto with zarith.
   apply Zlt_le_trans with (1:= U2).
@@ -349,7 +346,7 @@ Section GenDiv32.
     simpl;rewrite spec_sub.
     assert ([|a2|] - [|b2|] = wB*(-1) + ([|a2|] - [|b2|] + wB)). ring.
     assert (0 <= [|a2|] - [|b2|] + wB < wB). omega.
-    rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) U H1 H0).
+    rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) H1 H0).
     rewrite wwB_wBwB;ring.
    assert (U2 := wB_pos w_digits).
    eapply spec_ww_add_c_cont with (P :=
@@ -433,8 +430,8 @@ Section GenDiv32.
    rewrite <- H8 in H2;rewrite H2 in H7.
    assert (0 < [|b1|]*wB). apply Zmult_lt_0_compat;zarith.
    Spec_ww_to_Z r2. zarith.
-   rewrite (Zmod_def_small ([|q|] -1));zarith.
-   rewrite (Zmod_def_small ([|q|] -1 -1));zarith.
+   rewrite (Zmod_small ([|q|] -1));zarith.
+   rewrite (Zmod_small ([|q|] -1 -1));zarith.
    assert ([[r2]] + ([|b1|] * wB + [|b2|]) =
        wwB * 1 +
        ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2 * ([|b1|] * wB + [|b2|]))).
@@ -455,11 +452,10 @@ Section GenDiv32.
             wwB
             1
             ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2*([|b1|] * wB + [|b2|]))
-            U1
             H10 H8).
    split. ring. zarith.
    intros r2;repeat (rewrite spec_pred);simpl ww_to_Z;intros H7.
-   rewrite (Zmod_def_small ([|q|] -1));zarith.
+   rewrite (Zmod_small ([|q|] -1));zarith.
    split.
    replace [[r2]] with  ([[r1]] + ([|b1|] * wB + [|b2|]) -wwB).
    rewrite H2; ring. rewrite <- H7; ring.
@@ -580,7 +576,7 @@ Section GenDiv21.
    match goal with |-context [ww_compare ?Y ?Z] =>
      generalize (spec_ww_compare Y Z); case (ww_compare Y Z)
    end; simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith.
-   rewrite spec_ww_sub;simpl. rewrite Zmod_def_small;zarith.
+   rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith.
    split. ring.
    assert (wwB <= 2*[[b]]);zarith.
    rewrite wwB_div;zarith.
@@ -927,7 +923,7 @@ Section GenDivGt.
    Spec_ww_to_Z (WW ah al).
    rewrite spec_ww_sub;eauto.
    simpl;rewrite spec_ww_1;rewrite Zmult_1_l;simpl.
-   simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_def_small;split;zarith.
+   simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_small;split;zarith.
    case (spec_to_Z (w_head0 bh)); auto with zarith.
    assert ([|w_head0 bh|] < Zpos w_digits).
     destruct (Z_lt_ge_dec [|w_head0 bh|]  (Zpos w_digits));trivial.
@@ -951,8 +947,8 @@ Section GenDivGt.
    assert (H5:=to_Z_div_minus_p bl HHHH).
    rewrite Zmult_comm in Hh. 
    assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith.
-   unfold base in H0;rewrite Zmod_def_small;zarith.
-   fold wB; rewrite (Zmod_def_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith.
+   unfold base in H0;rewrite Zmod_small;zarith.
+   fold wB; rewrite (Zmod_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith.
    intros U1 U2 U3 V1 V2.
    generalize (@spec_w_div32 (w_add_mul_div (w_head0 bh) w_0 ah)
                (w_add_mul_div (w_head0 bh) ah al)
@@ -991,7 +987,7 @@ Section GenDivGt.
    Zmult_0_l;rewrite Zplus_0_l.
    replace [[ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry
        _ww_zdigits (w_0W (w_head0 bh))) W0 r]] with ([[r]]/2^[|w_head0 bh|]).
-   assert (0 < 2^[|w_head0 bh|]). apply Zpower_lt_0;zarith.
+   assert (0 < 2^[|w_head0 bh|]). apply Zpower_gt_0;zarith.
    split.
    rewrite <- (Z_div_mult [[WW ah al]] (2^[|w_head0 bh|]));zarith.
    rewrite H1;rewrite Zmult_assoc;apply Z_div_plus_l;trivial.
@@ -1002,9 +998,9 @@ Section GenDivGt.
    change (Zpos (xO (w_digits))) with (2*Zpos (w_digits));zarith.
    simpl ww_to_Z;rewrite Zmult_0_l;rewrite Zplus_0_l.
    rewrite spec_w_0W.
-   rewrite (fun x y => Zmod_def_small (x-y)); auto with zarith.
+   rewrite (fun x y => Zmod_small (x-y)); auto with zarith.
    ring_simplify (2 * Zpos w_digits - (2 * Zpos w_digits - [|w_head0 bh|])).
-   rewrite Zmod_def_small;zarith.
+   rewrite Zmod_small;zarith.
    split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith.
    Spec_ww_to_Z r.
    apply Zlt_le_trans with wwB;zarith.
@@ -1015,7 +1011,7 @@ Section GenDivGt.
    apply Zpower2_lt_lin; auto with zarith.
    rewrite spec_ww_sub; auto with zarith.
    rewrite spec_ww_digits_; rewrite spec_w_0W.
-   rewrite Zmod_def_small;zarith.
+   rewrite Zmod_small;zarith.
    rewrite Zpos_xO; split; auto with zarith.
    apply Zle_lt_trans with (2 * Zpos w_digits); auto with zarith.
    unfold base, ww_digits; rewrite (Zpos_xO w_digits).
@@ -1412,7 +1408,7 @@ Section GenDiv.
    intros a b Hpos;unfold ww_mod. 
    assert (H := spec_ww_compare a b);destruct (ww_compare a b).
    simpl;apply Zmod_unique with 1;try rewrite H;zarith.
-   Spec_ww_to_Z a;symmetry;apply Zmod_def_small;zarith.
+   Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith.
    apply spec_ww_mod_gt;trivial.
   Qed.
 
diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v
index 84bf247f75..7987741dad 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Ints/num/GenDivn1.v
@@ -9,8 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
+Require Import ZAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -230,7 +229,7 @@ Section GENDIVN1.
      with (2*Zpos (gen_digits w_digits n));auto with zarith.
    replace (2 ^ (Zpos (gen_digits w_digits (S n)) - [|p|])) with
     (2^(Zpos (gen_digits w_digits n) - [|p|])*2^Zpos (gen_digits w_digits n)).
-   rewrite Zdiv_Zmult_compat_r;auto with zarith.
+   rewrite Zdiv_mult_cancel_r;auto with zarith.
    rewrite Zmult_plus_distr_l with (p:=  2^[|p|]). 
    pattern  ([!n|hl!] * 2^[|p|]) at 2;
    rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))([|p|])([!n|hl!]));
@@ -254,7 +253,7 @@ Section GENDIVN1.
    with (2^Zpos(gen_digits w_digits n) *2^Zpos(gen_digits w_digits n)). 
    rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] +
       [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])))).
-   rewrite  Zmod_Zmult_compat_l;auto with zarith.
+   rewrite  Zmult_mod_distr_l;auto with zarith.
    ring. 
    rewrite Zpower_exp;auto with zarith.
    assert (0 < Zpos (gen_digits w_digits n)). unfold Zlt;reflexivity.
@@ -336,7 +335,7 @@ Section GENDIVN1.
   replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with
    (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * 
         2^Zpos (gen_digits w_digits n)).
-  rewrite Zdiv_Zmult_compat_r;auto with zarith.
+  rewrite Zdiv_mult_cancel_r;auto with zarith.
   rewrite <- Zpower_exp;auto with zarith.
   replace (Zpos (gen_digits w_digits n) - Zpos w_digits + 
     Zpos (gen_digits w_digits n)) with
@@ -373,7 +372,7 @@ Section GENDIVN1.
    generalize (spec_compare (w_head0 b) w_0); case w_compare;
      rewrite spec_0; intros H2; auto with zarith.
    assert (Hv1: wB/2 <= [|b|]).
-     generalize H0; rewrite H2; rewrite Zpower_exp_0;
+     generalize H0; rewrite H2; rewrite Zpower_0_r;
        rewrite Zmult_1_l; auto.
    assert (Hv2: [|w_0|] < [|b|]).
      rewrite spec_0; auto.
@@ -394,7 +393,7 @@ Section GENDIVN1.
     rewrite (spec_add_mul_div b w_0); auto with zarith.
     rewrite spec_0;rewrite Zdiv_0_l; try omega.
     rewrite Zplus_0_r; rewrite Zmult_comm.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
    assert (H5 := spec_to_Z (high n a)).
    assert 
     ([|w_add_mul_div (w_head0 b) w_0 (high n a)|]
@@ -407,15 +406,15 @@ Section GENDIVN1.
      apply Zlt_le_trans with wB;auto with zarith.
      pattern wB at 1;replace wB with (wB*1);try ring.
      apply Zmult_le_compat;auto with zarith.
-     assert (H6 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|]));
+     assert (H6 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));
        auto with zarith.
-    rewrite Zmod_def_small;auto with zarith.
+    rewrite Zmod_small;auto with zarith.
     apply Zdiv_lt_upper_bound;auto with zarith.
     apply Zlt_le_trans with wB;auto with zarith.
     apply Zle_trans with (2 ^ [|w_head0 b|] * [|b|] * 2).
     rewrite <- wB_div_2; try omega.
     apply Zmult_le_compat;auto with zarith.
-    pattern 2 at 1;rewrite <- Zpower_exp_1.
+    pattern 2 at 1;rewrite <- Zpower_1_r.
     apply Zpower_le_monotone;split;auto with zarith.
    rewrite <- H4 in H0. 
    assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. 
@@ -430,13 +429,13 @@ Section GENDIVN1.
    rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7.
    assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB
      = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - [|w_head0 b|])).
-   rewrite Zmod_def_small;auto with zarith.
+   rewrite Zmod_small;auto with zarith.
    rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
    replace (Zpos (gen_digits w_digits n) - Zpos w_digits + 
                        (Zpos w_digits - [|w_head0 b|]))
     with (Zpos (gen_digits w_digits n) - [|w_head0 b|]);trivial;ring.
-   assert (H8 := Zpower_lt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
+   assert (H8 := Zpower_gt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
    split;auto with zarith.
    apply Zle_lt_trans with ([|high n a|]);auto with zarith.
    apply Zdiv_le_upper_bound;auto with zarith.
@@ -451,20 +450,20 @@ Section GENDIVN1.
    rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l.
    replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) 
       with ([|w_head0 b|]).
-   rewrite Zmod_def_small;auto with zarith.
+   rewrite Zmod_small;auto with zarith.
    assert (H9 := spec_to_Z r).
    split;auto with zarith.
    apply Zle_lt_trans with ([|r|]);auto with zarith.
    apply Zdiv_le_upper_bound;auto with zarith.
    pattern ([|r|]) at 1;rewrite <- Zmult_1_r.
    apply Zmult_le_compat;auto with zarith.
-   assert (H10 := Zpower_lt_0 2  ([|w_head0 b|]));auto with zarith.
+   assert (H10 := Zpower_gt_0 2  ([|w_head0 b|]));auto with zarith.
    rewrite spec_sub.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    case (spec_to_Z w_zdigits); auto with zarith.
    rewrite spec_sub.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    case (spec_to_Z w_zdigits); auto with zarith.
   case H7; intros H71 H72.
diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v
index a7d8480ba6..06c76067eb 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Ints/num/GenLift.v
@@ -10,8 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZPowerAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -283,7 +281,7 @@ Section GenLift.
    repeat rewrite <- Zmult_assoc.
    apply f_equal2 with (f := Zmult); auto.
    case (spec_to_Z (w_tail0 xl)); intros HH3 HH4.
-   pattern 2 at 2; rewrite <- Zpower_exp_1.
+   pattern 2 at 2; rewrite <- Zpower_1_r.
    lazy beta; repeat rewrite <- Zpower_exp; auto with zarith.
    unfold base; apply f_equal with (f := Zpower 2); auto with zarith.
 
@@ -328,12 +326,12 @@ Section GenLift.
    fold wB.
    rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc.
    rewrite <- Zpower_2.
-   rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. apply lt_0_wwB. 
+   rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. 
    exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring.
    simpl ww_to_Z; w_rewrite;zarith.
    assert (HH0: [|low p|] = [[p]]).
      rewrite spec_low.
-     apply Zmod_def_small.
+     apply Zmod_small.
      case (spec_to_w_Z p); intros HH1 HH2; split; auto.
      generalize H1; unfold zdigits; rewrite spec_w_0W;
       rewrite spec_zdigits; intros tmp.
@@ -370,7 +368,7 @@ Section GenLift.
      rewrite spec_ww_sub.
      unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits.
      rewrite <- Zmod_div_mod; auto with zarith.
-     rewrite Zmod_def_small; auto with zarith.
+     rewrite Zmod_small; auto with zarith.
      split; auto with zarith.
      apply Zle_lt_trans with (Zpos w_digits); auto with zarith.
      unfold base; apply Zpower2_lt_lin; auto with zarith.
@@ -407,7 +405,7 @@ Section GenLift.
      ([|xh|]*2^u*wB). 2:ring.
    repeat rewrite <- Zplus_assoc. 
    rewrite (Zplus_comm ([|xh|] * 2 ^ u * wB)).
-   rewrite Z_mod_plus;zarith. rewrite Zmod_mult_0;zarith.
+   rewrite Z_mod_plus;zarith. rewrite Z_mod_mult;zarith.
    unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith.
    unfold u; split;zarith. 
    split;zarith. unfold u; apply Zdiv_lt_upper_bound;zarith.
@@ -450,7 +448,7 @@ Section GenLift.
    generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1.
    assert (HH0: [|low p|] = [[p]]).
      rewrite spec_low.
-     apply Zmod_def_small.
+     apply Zmod_small.
      case (spec_to_w_Z p); intros HH1 HH2; split; auto.
      apply Zlt_le_trans with (1 := H1).
      unfold base; apply Zpower2_le_lin; auto with zarith.
@@ -466,7 +464,7 @@ Section GenLift.
      rewrite spec_low.
      rewrite spec_ww_sub; w_rewrite; intros H1.
      rewrite <- Zmod_div_mod; auto with zarith.
-     rewrite Zmod_def_small; auto with zarith.
+     rewrite Zmod_small; auto with zarith.
      split; auto with zarith.
      apply Zle_lt_trans with (Zpos w_digits); auto with zarith.
      unfold base; apply Zpower2_lt_lin; auto with zarith.
diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v
index 7550781f16..5522e41bfc 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Ints/num/GenMul.v
@@ -10,7 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -327,7 +326,7 @@ Section GenMul.
    2:ring. rewrite <- H1;rewrite <- H;rewrite <- H0.  
    assert (H2 := sum_mul_carry _ _ _ _ _ _ H1).
    destruct cc as [ | cch ccl]; simpl zn2z_to_Z; simpl ww_to_Z.
-   rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_def_small;
+   rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_small;
     rewrite wwB_wBwB. ring.
    rewrite <- (Zplus_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith.
    simpl ww_to_Z in H1. assert (U:=spec_to_Z cch).
@@ -349,7 +348,7 @@ Section GenMul.
    as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Zmult_1_l;
    simpl zn2z_to_Z;
    try rewrite spec_ww_add;try rewrite spec_ww_add_carry;rewrite spec_w_WW;
-   rewrite Zmod_def_small;rewrite wwB_wBwB;intros.
+   rewrite Zmod_small;rewrite wwB_wBwB;intros.
    rewrite H4;ring. rewrite H;apply mult_add_ineq2;zarith.
    rewrite Zplus_assoc;rewrite Zmult_plus_distr_l.
    rewrite Zmult_1_l;rewrite <- Zplus_assoc;rewrite H4;ring.
@@ -385,8 +384,8 @@ Section GenMul.
 
   Lemma spec_w_2: [|w_2|] = 2.
   unfold w_2; rewrite spec_w_add; rewrite spec_w_1; simpl.
-  apply Zmod_def_small; split; auto with zarith.
-  rewrite <- (Zpower_exp_1 2); unfold base; apply Zpower_lt_monotone; auto with zarith.
+  apply Zmod_small; split; auto with zarith.
+  rewrite <- (Zpower_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith.
   Qed.
 
   Lemma kara_prod_aux : forall xh xl yh yl,
@@ -410,7 +409,7 @@ Section GenMul.
    generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
      try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
    repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    split; auto with zarith.
    simpl in Hz; rewrite Hz; rewrite H; rewrite H0.
    rewrite kara_prod_aux; apply Zplus_le_0_compat; apply Zmult_le_0_compat; auto with zarith.
@@ -422,10 +421,10 @@ Section GenMul.
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
      repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
      try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
@@ -433,12 +432,12 @@ Section GenMul.
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
      repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    split.
    match goal with |- context[(?x - ?y) * (?z - ?t)] =>
      replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring]
@@ -459,22 +458,22 @@ Section GenMul.
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l.
    generalize Hz2; clear Hz2; unfold interp_carry.
    repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
      generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1;
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_2; unfold interp_carry in Hz2.
    apply trans_equal with (wwB + (1 * wwB + [[z1]])).
    ring.
    rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
      try rewrite Hylh; try rewrite spec_w_1; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
@@ -482,25 +481,25 @@ Section GenMul.
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_2; unfold interp_carry in Hz2.
    apply trans_equal with (wwB + (1 * wwB + [[z1]])).
    ring.
    rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    match goal with |- context[ww_sub_c ?x ?y] =>
      generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1;
      intros z1 Hz2
    end.
    simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l.
    match goal with |- context[(?x - ?y) * (?z - ?t)] =>
      replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring]
    end.
    generalize Hz2; clear Hz2; unfold interp_carry.
    repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
-   repeat rewrite Zmod_def_small; auto with zarith; try (ring; fail).
+   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   Qed.
 
   Lemma sub_carry : forall xh xl yh yl z, 
@@ -539,21 +538,21 @@ Section GenMul.
    assert (U1:= lt_0_wwB w_digits).
    intros x y; case x; auto; intros xh xl.
    case y; auto.
-   simpl; rewrite Zmult_0_r; rewrite Zmod_def_small; auto with zarith.
+   simpl; rewrite Zmult_0_r; rewrite Zmod_small; auto with zarith.
    intros yh yl;simpl.
    repeat (rewrite spec_ww_add || rewrite spec_w_W0 || rewrite spec_w_mul_c
     || rewrite spec_w_add || rewrite spec_w_mul).
-   rewrite <- Zmod_plus; auto with zarith.
+   rewrite <- Zplus_mod; auto with zarith.
    repeat (rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r).
    rewrite <- Zmult_mod_distr_r; auto with zarith.
    rewrite <- Zpower_2; rewrite <- wwB_wBwB; auto with zarith.
-   rewrite Zmod_plus; auto with zarith.
+   rewrite Zplus_mod; auto with zarith.
    rewrite Zmod_mod; auto with zarith.
-   rewrite <- Zmod_plus; auto with zarith.
+   rewrite <- Zplus_mod; auto with zarith.
    match goal with |- ?X mod _ = _ =>
      rewrite <- Z_mod_plus with (a := X) (b := [|xh|] * [|yh|])
    end; auto with zarith.
-   eq_tac; auto; rewrite wwB_wBwB; ring.
+   f_equal; auto; rewrite wwB_wBwB; ring.
   Qed.
 
   Lemma spec_ww_square_c : forall x, [||ww_square_c x||] = [[x]]*[[x]].
@@ -607,7 +606,7 @@ Section GenMul.
    rewrite spec_w_0;trivial.
    assert (U:=spec_w_add_c l r);destruct (w_add_c l r) as [lr|lr];unfold
    interp_carry in U;try rewrite Zmult_1_l in H;simpl.
-   rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_def_small.
+   rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_small.
    rewrite <- Zplus_assoc;rewrite <- U;ring.
    simpl in H;assert (H1:= Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)).
    rewrite <- H in H1.
diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v
index 07b11ad749..3a5b59b6dc 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Ints/num/GenSqrt.v
@@ -10,8 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -277,10 +275,10 @@ Section GenSqrt.
 clear spec_more_than_1_digit. 
 intros x; case x; simpl ww_is_even.
  simpl.
- rewrite Zmod_def_small; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
  intros w1 w2; simpl.
  unfold base.
- rewrite Zmod_plus; auto with zarith.
+ rewrite Zplus_mod; auto with zarith.
  rewrite (fun x y => (Zdivide_mod (x * y))); auto with zarith.
  rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
  apply spec_w_is_even; auto with zarith.
@@ -313,12 +311,12 @@ intros x; case x; simpl ww_is_even.
  destruct (spec_to_Z a2);auto with zarith.
  intros H1 H2; split.
  unfold interp_carry; autorewrite with w_rewrite rm10; auto with zarith.
- rewrite H2; rewrite Zmod_def_small; auto with zarith.
+ rewrite H2; rewrite Zmod_small; auto with zarith.
  ring.
  destruct (spec_to_Z a2);auto with zarith.
  rewrite spec_w_sub; auto with zarith.
  destruct (spec_to_Z a2) as [H3 H4];auto with zarith.
- rewrite Zmod_def_small; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
  split; auto with zarith.
  assert ([|a2|] < 2 * [|b|]); auto with zarith.
  apply Zlt_le_trans with (2 * (wB / 2)); auto with zarith.
@@ -332,7 +330,7 @@ intros x; case x; simpl ww_is_even.
  intros H1.
  assert (H2: [|w_sub a1 b|] < [|b|]).
  rewrite spec_w_sub; auto with zarith.
- rewrite Zmod_def_small; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
  assert ([|a1|] < 2 * [|b|]); auto with zarith.
  apply Zlt_le_trans with (2 * (wB / 2)); auto with zarith.
  rewrite wB_div_2; auto.
@@ -344,7 +342,7 @@ intros x; case x; simpl ww_is_even.
    auto
  end.
  intros w0 w1; replace [+|C1 w0|] with (wB + [|w0|]).
- rewrite Zmod_def_small; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
  intros (H3, H4); split; auto.
  rewrite Zmult_plus_distr_l.
  rewrite <- Zplus_assoc; rewrite <- H3; ring.
@@ -366,7 +364,7 @@ intros x; case x; simpl ww_is_even.
  intros w1.
  assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1).
    rewrite spec_pred; rewrite spec_w_zdigits.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    apply Zlt_le_trans with (Zpos w_digits); auto with zarith.
    unfold base; apply Zpower2_le_lin; auto with zarith.
@@ -375,7 +373,7 @@ intros x; case x; simpl ww_is_even.
  match goal with |- context[?X - ?Y] =>
   replace (X - Y) with 1
  end.
- rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith.
+ rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith.
  destruct (spec_to_Z w1) as [H1 H2];auto with zarith.
  split; auto with zarith. 
  apply Zdiv_lt_upper_bound; auto with zarith.  
@@ -388,7 +386,7 @@ intros x; case x; simpl ww_is_even.
  intros w1.
  assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1).
    rewrite spec_pred; rewrite spec_w_zdigits.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    apply Zlt_le_trans with (Zpos w_digits); auto with zarith.
    unfold base; apply Zpower2_le_lin; auto with zarith.
@@ -397,7 +395,8 @@ intros x; case x; simpl ww_is_even.
   replace (X - Y) with 1
  end; rewrite Hp; try ring.
  rewrite Zpos_minus; auto with zarith.
- rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
+ rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith.
  destruct (spec_to_Z w1) as [H1 H2];auto with zarith.
  split; auto with zarith. 
  unfold base.
@@ -405,14 +404,14 @@ intros x; case x; simpl ww_is_even.
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite <- (tmp X); clear tmp
  end.
- rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith.
+ rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
  assert (tmp: forall p, 1 + (p -1) - 1 = p - 1); auto with zarith;
   rewrite tmp; clear tmp; auto with zarith.
  match goal with |- ?X + ?Y < _ =>
  assert (Y < X); auto with zarith
  end.
  apply Zdiv_lt_upper_bound; auto with zarith.
- pattern 2 at 2; rewrite <- Zpower_exp_1; rewrite <- Zpower_exp;
+ pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp;
   auto with zarith.
  assert (tmp: forall p, (p - 1) + 1 = p); auto with zarith;
   rewrite tmp; clear tmp; auto with zarith.
@@ -422,7 +421,7 @@ intros x; case x; simpl ww_is_even.
     [|w_add_mul_div w_1 w w_0|] = 2 * [|w|] mod wB.
  intros w1.
  autorewrite with w_rewrite rm10; auto with zarith.
- rewrite Zpower_exp_1; auto with zarith.
+ rewrite Zpower_1_r; auto with zarith.
  rewrite Zmult_comm; auto.
  Qed.
 
@@ -432,7 +431,7 @@ intros x; case x; simpl ww_is_even.
  rewrite spec_ww_add_mul_div; auto with zarith.
  autorewrite with w_rewrite rm10.
  rewrite spec_w_0W; rewrite spec_w_1. 
- rewrite Zpower_exp_1; auto with zarith.
+ rewrite Zpower_1_r; auto with zarith.
  rewrite Zmult_comm; auto.
  rewrite spec_w_0W; rewrite spec_w_1; auto with zarith.
  red; simpl; intros; discriminate.
@@ -444,22 +443,18 @@ intros x; case x; simpl ww_is_even.
  intros w1.
  rewrite spec_ww_add_mul_div; auto with zarith.
  rewrite spec_w_0W; rewrite spec_w_1; auto with zarith.
- rewrite Zpower_exp_1; auto with zarith.
- eq_tac; auto.
- rewrite Zmult_comm; eq_tac; auto.
+ rewrite Zpower_1_r; auto with zarith.
+ f_equal; auto.
+ rewrite Zmult_comm; f_equal; auto.
  autorewrite with w_rewrite rm10.
  unfold ww_digits, base.
  apply sym_equal; apply Zdiv_unique with (r := 2 ^ (Zpos (ww_digits w_digits) - 1) -1);
   auto with zarith.
- apply Zpower_lt_0; auto with zarith. 
- match goal with  |- 0 <= ?X - 1 =>
-   assert (0 < X); auto with zarith; red; reflexivity
- end.
  unfold ww_digits; split; auto with zarith.
  match goal with  |- 0 <= ?X - 1 =>
    assert (0 < X); auto with zarith
  end.
- apply Zpower_lt_0; auto with zarith. 
+ apply Zpower_gt_0; auto with zarith. 
  match goal with  |- 0 <= ?X - 1 =>
    assert (0 < X); auto with zarith; red; reflexivity
  end.
@@ -468,8 +463,8 @@ intros x; case x; simpl ww_is_even.
   rewrite tmp; clear tmp.
  assert (tmp: forall p, p + p = 2 * p); auto with zarith;
   rewrite tmp; clear tmp.
- eq_tac; auto.
- pattern 2 at 2; rewrite <- Zpower_exp_1; rewrite <- Zpower_exp;
+ f_equal; auto.
+ pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp;
   auto with zarith.
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite tmp; clear tmp; auto.
@@ -480,8 +475,8 @@ intros x; case x; simpl ww_is_even.
  red; simpl; intros; discriminate.
  Qed.
 
- Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1.
- intros a1 b1 H; rewrite Zmod_plus; auto with zarith.
+ Theorem Zplus_mod_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1.
+ intros a1 b1 H; rewrite Zplus_mod; auto with zarith.
  rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith.
  apply Zmod_mod; auto.
  Qed.
@@ -544,9 +539,10 @@ intros x; case x; simpl ww_is_even.
  match goal with |- context[_ ^ ?X] =>
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; 
-  try rewrite Zpower_exp_1; auto with zarith
+  try rewrite Zpower_1_r; auto with zarith
  end.
  rewrite Zpos_minus; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
  ring.
  repeat rewrite C0_id.
  rewrite spec_w_add_c; auto with zarith.
@@ -560,9 +556,10 @@ intros x; case x; simpl ww_is_even.
  match goal with |- context[_ ^ ?X] =>
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; 
-  try rewrite Zpower_exp_1; auto with zarith
+  try rewrite Zpower_1_r; auto with zarith
  end.
  rewrite Zpos_minus; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
  ring.
  repeat rewrite C1_plus_wB in H0.
  rewrite C1_plus_wB.
@@ -573,8 +570,8 @@ intros x; case x; simpl ww_is_even.
  end.
  intros c w1; case c.
  intros w2 (Hw1, Hw2); rewrite C0_id in Hw1.
- rewrite <- Zmod_plus_one in Hw1; auto with zarith.
- rewrite Zmod_def_small in Hw1; auto with zarith.
+ rewrite <- Zplus_mod_one in Hw1; auto with zarith.
+ rewrite Zmod_small in Hw1; auto with zarith.
  match goal with |- context[w_is_even ?y] =>
    generalize (spec_w_is_even y);
    case (w_is_even y)
@@ -592,9 +589,10 @@ intros x; case x; simpl ww_is_even.
  match goal with |- context[_ ^ ?X] =>
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; 
-  try rewrite Zpower_exp_1; auto with zarith
+  try rewrite Zpower_1_r; auto with zarith
  end.
  rewrite Zpos_minus; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
  ring.
  repeat rewrite C0_id.
  rewrite add_mult_div_2_plus_1.
@@ -610,9 +608,10 @@ intros x; case x; simpl ww_is_even.
  match goal with |- context[_ ^ ?X] =>
  assert (tmp: forall p, 1 + (p - 1) = p); auto with zarith;
   rewrite <- (tmp X); clear tmp; rewrite Zpower_exp; 
-  try rewrite Zpower_exp_1; auto with zarith
+  try rewrite Zpower_1_r; auto with zarith
  end.
  rewrite Zpos_minus; auto with zarith.
+ rewrite Zmax_right; auto with zarith.
  ring.
  split; auto with zarith.
  destruct (spec_to_Z b);auto with zarith.
@@ -620,8 +619,8 @@ intros x; case x; simpl ww_is_even.
  destruct (spec_to_Z b);auto with zarith.
  destruct (spec_to_Z b);auto with zarith.
  intros w2; rewrite C1_plus_wB.
- rewrite <- Zmod_plus_one; auto with zarith.
- rewrite Zmod_def_small; auto with zarith.
+ rewrite <- Zplus_mod_one; auto with zarith.
+ rewrite Zmod_small; auto with zarith.
  intros (Hw1, Hw2).
  match goal with |- context[w_is_even ?y] =>
    generalize (spec_w_is_even y);
@@ -662,7 +661,7 @@ intros x; case x; simpl ww_is_even.
               4 * (2 ^ (Zpos w_digits - 2))).
   change 4 with (2 ^ 2).
   rewrite <- Zpower_exp; auto with zarith.
-  eq_tac; auto with zarith.
+  f_equal; auto with zarith.
   rewrite H.
   rewrite (fun x => (Zmult_comm 4 (2 ^x))).
   rewrite Z_div_mult; auto with zarith.
@@ -670,7 +669,7 @@ intros x; case x; simpl ww_is_even.
 
  Theorem Zsquare_mult: forall p, p ^ 2 = p * p.
  intros p; change 2 with (1 + 1); rewrite Zpower_exp;
-  try rewrite Zpower_exp_1; auto with zarith.
+  try rewrite Zpower_1_r; auto with zarith.
  Qed.
 
  Theorem Zsquare_pos: forall p, 0 <= p ^ 2.
@@ -817,7 +816,7 @@ intros x; case x; simpl ww_is_even.
  rewrite spec_ww_pred.
  rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]);
   auto with zarith.
- intros Hz1; rewrite Zmod_def_small; auto with zarith.
+ intros Hz1; rewrite Zmod_small; auto with zarith.
  match type of H5 with -?X + ?Y = ?Z =>
   assert (V: Y = Z + X);
   try (rewrite <- H5; ring)
@@ -866,7 +865,7 @@ intros x; case x; simpl ww_is_even.
  rewrite spec_ww_add; auto with zarith.
  rewrite spec_ww_pred; auto with zarith.
  rewrite ww_add_mult_mult_2.
- assert (VV1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)).
+ rename V1 into VV1.
  assert (VV2: 0 <  [[WW w4 w5]]); auto with zarith.
  apply Zlt_le_trans with (wB/ 2 * wB + 0); auto with zarith.
  autorewrite with rm10; apply Zmult_lt_0_compat; auto with zarith.
@@ -886,7 +885,7 @@ intros x; case x; simpl ww_is_even.
  simpl ww_to_Z; assert (V4 := spec_to_Z w5);auto with zarith.
  rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]);
   auto with zarith.
- intros Hz1; rewrite Zmod_def_small; auto with zarith.
+ intros Hz1; rewrite Zmod_small; auto with zarith.
  match type of H5 with -?X + ?Y = ?Z =>
   assert (V: Y = Z + X);
   try (rewrite <- H5; ring)
@@ -895,7 +894,7 @@ intros x; case x; simpl ww_is_even.
   assert (V1: Y = Z - 1);
   [replace (Z - 1) with (X + (-X + Z -1));
     [rewrite <- Hz1 | idtac]; ring
-   |  idtac]
+    | idtac]
  end.
  rewrite <- Zmod_unique with (q := 1) (r := -wwB + [[z1]] + [[z]]);
   auto with zarith.
@@ -1161,24 +1160,24 @@ intros x; case x; simpl ww_is_even.
   assert (Hp0: 0 < [[ww_head0 x]]).
     generalize (spec_ww_is_even (ww_head0 x)); rewrite H1.
     generalize Hv1; case [[ww_head0 x]].
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
     intros; assert (0 < Zpos p); auto with zarith.
     red; simpl; auto.
     intros p H2; case H2; auto.
   assert (Hp: [[ww_pred (ww_head0 x)]] = [[ww_head0 x]] - 1).
     rewrite spec_ww_pred.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
   intros H2; split.
     generalize (spec_ww_is_even (ww_pred (ww_head0 x)));
       case ww_is_even; auto.
     rewrite Hp.
-    rewrite Zmod_minus; auto with zarith.
-    rewrite H2; repeat rewrite Zmod_def_small; auto with zarith.
+    rewrite Zminus_mod; auto with zarith.
+    rewrite H2; repeat rewrite Zmod_small; auto with zarith.
   intros H3; rewrite Hp.  
   case (spec_ww_head0 x); auto; intros Hv3 Hv4.
   assert (Hu: forall u, 0 < u -> 2 *  2 ^ (u - 1) = 2 ^u).
     intros u Hu.
-    pattern 2 at 1; rewrite <- Zpower_exp_1.
+    pattern 2 at 1; rewrite <- Zpower_1_r.
     rewrite <- Zpower_exp; auto with zarith.
     ring_simplify (1 + (u - 1)); auto with zarith.
   split; auto with zarith.
@@ -1254,13 +1253,13 @@ intros x; case x; simpl ww_is_even.
   generalize (spec_ww_add_mul_div x W0 (ww_head1 x) Hv2);
      case ww_add_mul_div.
   simpl ww_to_Z; autorewrite with w_rewrite rm10.
-  rewrite Zmod_def_small; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
   intros H2; case (Zmult_integral _ _ (sym_equal H2)); clear H2; intros H2.
   rewrite H2; unfold Zpower, Zpower_pos; simpl; auto with zarith.
   match type of H2 with ?X = ?Y =>
    absurd (Y < X); try (rewrite H2; auto with zarith; fail)
   end.
-  apply Zpower_lt_0; auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
   split; auto with zarith.
   case Hp2; intros _ tmp; apply Zle_lt_trans with (2 := tmp);
    clear tmp.
@@ -1271,7 +1270,7 @@ intros x; case x; simpl ww_is_even.
     generalize (spec_ww_is_even (ww_head1 x)); rewrite Hp1;
       intros tmp; rewrite tmp; rewrite Zplus_0_r; auto.
   intros w0 w1; autorewrite with w_rewrite rm10.
-  rewrite Zmod_def_small; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
   2: rewrite Zmult_comm; auto with zarith.
   intros H2.
   assert (V: wB/4 <= [|w0|]).
@@ -1287,7 +1286,7 @@ intros x; case x; simpl ww_is_even.
   assert (Hv3: [[ww_pred ww_zdigits]]
                  = Zpos (xO w_digits) - 1).
     rewrite spec_ww_pred; rewrite spec_ww_zdigits.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
     split; auto with zarith.
     apply Zlt_le_trans with (Zpos (xO w_digits)); auto with zarith.
     unfold base; apply Zpower2_le_lin; auto with zarith.  
@@ -1303,8 +1302,8 @@ intros x; case x; simpl ww_is_even.
     simpl ww_to_Z; autorewrite with rm10.
     rewrite Hv3.
     ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)).
-    rewrite Zpower_exp_1.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zpower_1_r.
+    rewrite Zmod_small; auto with zarith.
     split; auto with zarith.
     apply Zlt_le_trans with (1 := Hv4); auto with zarith.
     unfold base; apply Zpower_le_monotone; auto with zarith.
@@ -1313,15 +1312,15 @@ intros x; case x; simpl ww_is_even.
   assert (Hv6: [|low(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))|]
                  = [[ww_head1 x]]/2).
     rewrite spec_low.
-    rewrite Hv5; rewrite Zmod_def_small; auto with zarith.
+    rewrite Hv5; rewrite Zmod_small; auto with zarith.
   rewrite spec_w_add_mul_div; auto with zarith.
   rewrite spec_w_sub; auto with zarith.
   rewrite spec_w_0.
   simpl ww_to_Z; autorewrite with rm10.
   rewrite Hv6; rewrite spec_w_zdigits.
-  rewrite (fun x y => Zmod_def_small (x - y)).
+  rewrite (fun x y => Zmod_small (x - y)).
   ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)).
-  rewrite Zmod_def_small.
+  rewrite Zmod_small.
   simpl ww_to_Z in H2; rewrite H2; auto with zarith.
   intros (H4, H5); split.
   apply Zmult_le_reg_r with (2 ^ [[ww_head1 x]]); auto with zarith.
@@ -1335,7 +1334,7 @@ intros x; case x; simpl ww_is_even.
   assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2);
    try (intros; repeat rewrite Zsquare_mult; ring);
    rewrite tmp; clear tmp.
-  apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith.
+  apply Zpower_le_monotone3; auto with zarith.
   split; auto with zarith.
   pattern [|w2|] at 2; 
      rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]] / 2)));
@@ -1361,7 +1360,7 @@ intros x; case x; simpl ww_is_even.
   assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2);
    try (intros; repeat rewrite Zsquare_mult; ring);
    rewrite tmp; clear tmp.
-  apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith.
+  apply Zpower_le_monotone3; auto with zarith.
   split; auto with zarith.
   pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]]/2)));
     auto with zarith.
@@ -1375,7 +1374,7 @@ intros x; case x; simpl ww_is_even.
     auto with zarith.
   apply Zmult_le_compat_l; auto with zarith.
   apply Zpower_le_monotone; auto with zarith.
-  rewrite Zpower_exp_0; autorewrite with rm10; auto.
+  rewrite Zpower_0_r; autorewrite with rm10; auto.
   split; auto with zarith.
   rewrite Hv0 in Hv2; rewrite (Zpos_xO w_digits) in Hv2; auto with zarith.
   apply Zle_lt_trans with (Zpos w_digits); auto with zarith.
@@ -1383,7 +1382,7 @@ intros x; case x; simpl ww_is_even.
   rewrite spec_w_sub; auto with zarith.
   rewrite Hv6; rewrite spec_w_zdigits; auto with zarith.
   assert (Hv7: 0 < [[ww_head1 x]]/2); auto with zarith.
-  rewrite Zmod_def_small; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
   split; auto with zarith.
   assert ([[ww_head1 x]]/2 <= Zpos w_digits); auto with zarith.
   apply Zmult_le_reg_r with 2; auto with zarith.
diff --git a/theories/Ints/num/GenSub.v b/theories/Ints/num/GenSub.v
index 43661edd5b..9b09248532 100644
--- a/theories/Ints/num/GenSub.v
+++ b/theories/Ints/num/GenSub.v
@@ -10,7 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -221,7 +220,7 @@ Section GenSub.
    rewrite H0;rewrite Zplus_0_r; rewrite Zpower_2;
     rewrite Zmult_mod_distr_r;try apply lt_0_wB.
    rewrite spec_opp;trivial.
-   apply Zmod_unique with (q:= -1). apply lt_0_wwB.
+   apply Zmod_unique with (q:= -1).
    exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW (w_opp_carry xh) l)).
    rewrite spec_opp_carry;rewrite wwB_wBwB;ring.
   Qed.
@@ -295,12 +294,12 @@ Section GenSub.
   Lemma spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB.
   Proof.
    destruct x as [ |xh xl];simpl. 
-   apply Zmod_unique with (-1). apply lt_0_wwB. apply spec_ww_to_Z;trivial.
+   apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial.
    rewrite spec_ww_Bm1;ring.
    replace ([|xh|]*wB + [|xl|] - 1) with ([|xh|]*wB + ([|xl|] - 1)). 2:ring.
    generalize (spec_pred_c xl);destruct (w_pred_c xl) as [l|l];intro H;
    unfold interp_carry in H;rewrite <- H;simpl ww_to_Z.
-   rewrite Zmod_def_small. apply spec_w_WW. 
+   rewrite Zmod_small. apply spec_w_WW. 
    exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh l)).
    rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. 
    change ([|xh|] + -1) with ([|xh|] - 1).
@@ -313,7 +312,7 @@ Section GenSub.
   Lemma spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
   Proof.
    destruct y as [ |yh yl];simpl.
-   ring_simplify ([[x]] - 0);rewrite Zmod_def_small;trivial. apply spec_ww_to_Z;trivial.
+   ring_simplify ([[x]] - 0);rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial.
    destruct x as [ |xh xl];simpl. exact (spec_ww_opp (WW yh yl)).
    replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|])) 
    with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|])). 2:ring.
@@ -331,7 +330,7 @@ Section GenSub.
    destruct y as [ |yh yl];simpl.
    ring_simplify ([[x]] - 0);exact (spec_ww_pred x).
    destruct x as [ |xh xl];simpl.
-   apply Zmod_unique with (-1). apply lt_0_wwB.
+   apply Zmod_unique with (-1).
    apply spec_ww_to_Z;trivial.
    fold (ww_opp_carry (WW yh yl)).
    rewrite (spec_ww_opp_carry (WW yh yl));simpl ww_to_Z;ring.
diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v
index f7731ae6a6..0d85c92ed1 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Ints/num/Nbasic.v
@@ -1,6 +1,5 @@
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import Max.
 Require Import GenBase.
@@ -28,13 +27,13 @@ assert (tmp: (forall p, 2 * p = p + p)%Z);
 intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
 assert (tmp: (forall p, 2 * p = p + p)%Z); 
   try repeat rewrite tmp; auto with zarith.
-rewrite ZPowerAux.Zpower_exp_1; auto with zarith.
+rewrite Zpower_1_r; auto with zarith.
 Qed.
 
 Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
 intros p; case (Psucc_pred p); intros H1.
 subst; simpl plength.
-rewrite ZPowerAux.Zpower_exp_1; auto with zarith.
+rewrite Zpower_1_r; auto with zarith.
 pattern p at 1; rewrite <- H1.
 rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
 generalize (plength_correct (Ppred p)); auto with zarith.
@@ -296,7 +295,7 @@ Section CompareRec.
  Lemma base_xO: forall n, base (xO n) = (base n)^2.
  Proof.
  intros n1; unfold base.
- rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite ZAux.Zpower_mult; auto with zarith.
+ rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
  Qed.
 
  Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n :=
diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v
index 326e629024..c39a63301a 100644
--- a/theories/Ints/num/Q0Make.v
+++ b/theories/Ints/num/Q0Make.v
@@ -2,7 +2,6 @@ Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v
index 53fb65b2a8..fdf8647079 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Ints/num/QbiMake.v
@@ -2,7 +2,6 @@ Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v
index add89898a8..5f461aa59b 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Ints/num/QifMake.v
@@ -2,7 +2,6 @@ Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v
index 3c859d0f12..906cf8d159 100644
--- a/theories/Ints/num/QpMake.v
+++ b/theories/Ints/num/QpMake.v
@@ -2,7 +2,6 @@ Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v
index eb97123da3..e51291a041 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Ints/num/QvMake.v
@@ -2,7 +2,6 @@ Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v
index 0a2b5cd3fd..d00f14ec6c 100644
--- a/theories/Ints/num/ZMake.v
+++ b/theories/Ints/num/ZMake.v
@@ -1,6 +1,5 @@
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 
 Open Scope Z_scope.
 
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v
index db3f28b418..a244635ea8 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Ints/num/Zn2Z.v
@@ -10,7 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenAdd.
@@ -588,7 +587,7 @@ Section Zn2Z.
    _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto.
   unfold w_Bm2, w_to_Z, w_pred, w_Bm1.
   rewrite (spec_pred op_spec);rewrite (spec_Bm1 op_spec).
-  unfold w_digits;rewrite Zmod_def_small. ring.
+  unfold w_digits;rewrite Zmod_small. ring.
   assert (H:= wB_pos(znz_digits w_op)). omega.
   exact (spec_WW op_spec). exact (spec_compare op_spec).
   exact (spec_mul_c op_spec).  exact (spec_div21 op_spec).
@@ -621,12 +620,12 @@ Section Zn2Z.
   w_to_Z (low x) = [|x|] mod wB.
   intros x; case x; simpl low.
     unfold ww_to_Z, w_to_Z, w_0; rewrite (spec_0 op_spec); simpl.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
     split; auto with zarith.
     unfold wB, base; auto with zarith.
   intros xh xl; simpl.
   rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith.
-  rewrite Zmod_def_small; auto with zarith.
+  rewrite Zmod_small; auto with zarith.
   unfold wB, base; auto with zarith.
  Qed.
 
diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v
index 68f1092cdf..61d1ced604 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Ints/num/ZnZ.v
@@ -8,7 +8,6 @@
 
 Set Implicit Arguments.
 
-Require Import Tactic.
 Require Import ZArith.
 Require Import Znumtheory.
 Require Import Basic_type.