4 files changed, 30 insertions, 12 deletions
diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v
index 9fa37721a..c2885bc77 100644
--- a/src/Arithmetic/BarrettReduction/Generalized.v
+++ b/src/Arithmetic/BarrettReduction/Generalized.v
@@ -9,7 +9,15 @@
     base ([b]), exponent ([k]), and the [offset] than those given in
     the HAC. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Pow.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.ZSimplify.
+Require Import Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
 
@@ -94,17 +102,17 @@ Section barrett.
       : q * n <= a.
     Proof using a_nonneg a_small base_good k_big_enough m_good n_pos n_reasonable offset_nonneg.
       subst q r m.
-      assert (0 < b^(k-offset)). zero_bounds.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(2 * k)) by zero_bounds.
+      assert (0 < b^(k-offset)). Z.zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(2 * k)) by Z.zero_bounds.
       Z.simplify_fractions_le.
       autorewrite with pull_Zpow pull_Zdiv zsimplify; reflexivity.
     Qed.
 
     Lemma q_nice : { b : bool * bool | q = a / n + (if fst b then -1 else 0) + (if snd b then -1 else 0) }.
     Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(k-offset)) by zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(k-offset)) by Z.zero_bounds.
       assert (a / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia.
       assert (a / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption).
       subst q r m.
diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v
index 70661ee96..c9fb2f16f 100644
--- a/src/Arithmetic/BarrettReduction/HAC.v
+++ b/src/Arithmetic/BarrettReduction/HAC.v
@@ -9,7 +9,13 @@
     have to carry around extra precision), but requires more stringint
     conditions on the base ([b]), exponent ([k]), and the [offset]. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.ZSimplify.
 
 Local Open Scope Z_scope.
 
@@ -72,8 +78,8 @@ Section barrett.
     Let R := x mod m.
     Lemma q3_nice : { b : bool * bool | q3 = Q + (if fst b then -1 else 0) + (if snd b then -1 else 0) }.
     Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg x_nonneg x_small μ_good.
-      assert (0 < b^(k+offset)) by zero_bounds.
-      assert (0 < b^(k-offset)) by zero_bounds.
+      assert (0 < b^(k+offset)) by Z.zero_bounds.
+      assert (0 < b^(k-offset)) by Z.zero_bounds.
       assert (x / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia.
       assert (x / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption).
       subst q1 q2 q3 Q r_mod_3m r_mod_3m_orig r1 r2 R μ.
diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v
index b9697839d..af030dcfe 100644
--- a/src/Arithmetic/BarrettReduction/RidiculousFish.v
+++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.ZArith.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
diff --git a/src/Arithmetic/BarrettReduction/Wikipedia.v b/src/Arithmetic/BarrettReduction/Wikipedia.v
index 69ce10c4b..46f831281 100644
--- a/src/Arithmetic/BarrettReduction/Wikipedia.v
+++ b/src/Arithmetic/BarrettReduction/Wikipedia.v
@@ -1,7 +1,11 @@
 (*** Barrett Reduction *)
 (** This file implements Barrett Reduction on [Z].  We follow Wikipedia. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
@@ -80,7 +84,7 @@ Section barrett.
       : q * n <= a.
     Proof using a_nonneg k_good m_good n_pos n_reasonable.
       pose proof k_nonnegative; subst q r m.
-      assert (0 <= 2^(k-1)) by zero_bounds.
+      assert (0 <= 2^(k-1)) by Z.zero_bounds.
       Z.simplify_fractions_le.
     Qed.