9 files changed, 36 insertions, 14 deletions
diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v
index e6dbb01ed..c38eadd9c 100644
--- a/src/Compilers/Named/MapCastInterp.v
+++ b/src/Compilers/Named/MapCastInterp.v
@@ -11,7 +11,6 @@ Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
 Require Import Crypto.Compilers.Named.InterpSideConditions.
 Require Import Crypto.Compilers.Named.InterpSideConditionsInterp.
 Require Import Crypto.Compilers.Named.MapCast.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v
index b04613fa7..eb141cad1 100644
--- a/src/Compilers/Named/MapCastWf.v
+++ b/src/Compilers/Named/MapCastWf.v
@@ -11,7 +11,6 @@ Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Compilers.Named.MapCast.
 Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index c34089a60..c1c841c9f 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -10,8 +10,17 @@ Require Import Crypto.Compilers.Z.OpInversion.
 Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
 Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil.
 Require Import Crypto.Compilers.Z.Syntax.Equality.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Z2Nat.
 Require Import Crypto.Util.ZUtil.AddGetCarry.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sum.
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index ff690688a..4efa7445a 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -10,7 +10,6 @@ Require Import Crypto.Compilers.Z.OpInversion.
 Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
 Require Import Crypto.Compilers.Z.Syntax.Equality.
 Require Import Crypto.Compilers.Z.Syntax.Util.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sum.
 Require Import Crypto.Util.Prod.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 45566839a..b23e0ff1b 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -8,9 +8,13 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Stabilization.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
index 1701b4688..7ffe0beb1 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
@@ -7,7 +7,12 @@ Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
 Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Pow2.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
 Require Import Crypto.Util.Option.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
index 71f4b758b..6486b2e00 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
@@ -1,7 +1,14 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Psatz.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Shift.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Notations.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v
index 328ea5f48..8178592ed 100644
--- a/src/Compilers/Z/Bounds/Relax.v
+++ b/src/Compilers/Z/Bounds/Relax.v
@@ -15,7 +15,8 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Option.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Bool.
 
 Local Lemma helper logsz v
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index a4f5506fe..110e6b816 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Wf.
@@ -6,9 +7,7 @@ Require Import Crypto.Compilers.TypeUtil.
 Require Import Crypto.Compilers.TypeInversion.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Util.FixedWordSizesEquality.
-Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.HProp.
-Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Notations.
@@ -113,8 +112,8 @@ Proof.
                  | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H
                  | [ H : TWord _ = TWord _ |- _ ] => inversion H; clear H
                  end
-               | rewrite ZToWord_wordToZ_ZToWord by omega *
-               | rewrite wordToZ_ZToWord_wordToZ by omega *
+               | rewrite ZToWord_wordToZ_ZToWord by lia
+               | rewrite wordToZ_ZToWord_wordToZ by lia
                | rewrite wordToZ_ZToWord by assumption
                | rewrite ZToWord_wordToZ_ZToWord_small by omega ].
 Qed.
@@ -182,8 +181,8 @@ Proof.
                  | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H
                  | [ H : TWord _ = TWord _ |- _ ] => inversion H; clear H
                  end
-               | rewrite ZToWord_wordToZ_ZToWord by omega *
-               | rewrite wordToZ_ZToWord_wordToZ by omega * ].
+               | rewrite ZToWord_wordToZ_ZToWord by lia
+               | rewrite wordToZ_ZToWord_wordToZ by lia ].
 Qed.
 
 Lemma ZToInterp_eq_inj {a} x y