update _CoqProject, fix indentations, and prune dependencies of new Arithmetic files

10 files changed, 583 insertions, 598 deletions

diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v
index c5cc1ecde..b679a168c 100644
--- a/src/Arithmetic/BarrettReduction.v
+++ b/src/Arithmetic/BarrettReduction.v
@@ -1,61 +1,29 @@
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
 Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
+Require Import Coq.Lists.List.
+Require Import Crypto.Algebra.Ring.
+Require Import Crypto.Arithmetic.BaseConversion.
+Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.Partition.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Arithmetic.Saturated.
+Require Import Crypto.Arithmetic.UniformWeight.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.AddModulo.
+Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
+Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
+
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Import ListNotations. Local Open Scope Z_scope.
 
 Section Generic.
   Context (b k M mu width : Z) (n : nat)
@@ -66,8 +34,8 @@ Section Generic.
           (mu_eq : mu = b ^ (2 * k) / M)
           (width_pos : 0 < width)
           (strong_bound : b ^ 1 * (b ^ (2 * k) mod M) <= b ^ (k + 1) - mu).
-  Local Notation weight := (UniformWeight.uweight width).
-  Local Notation partition := (Partition.partition weight).
+  Local Notation weight := (uweight width).
+  Local Notation partition := (partition weight).
   Context (q1 : list Z -> list Z)
           (q1_correct :
              forall x,
@@ -389,9 +357,6 @@ Module Fancy.
         apply Z.pow_le_mono_r; lia.
       Qed.
 
-      (* use zero_bounds in zutil_arith *)
-      Local Ltac zutil_arith ::= solve [ omega | Psatz.lia | auto with nocore | solve [Z.zero_bounds] ].
-
       Lemma muSelect_correct x :
         0 <= x < w (sz * 2) ->
         muSelect (partition w (sz*2) x) = partition w sz (mu mod (w sz) * (x / 2 ^ (k - 1) / (w sz))).
@@ -406,7 +371,8 @@ Module Fancy.
                  | H : 0 <= ?x < ?m |- context [?x mod ?m] => rewrite (Z.mod_small x m) by auto with zarith
                  end.
         replace (x / (w (sz * 2 - 1)) / (2 ^ width / 2)) with (x / (2 ^ (k - 1)) / w sz) by
-            (autorewrite with weight_to_pow pull_Zpow pull_Zdiv; do 2 f_equal; nia).
+            (autorewrite with weight_to_pow pull_Zpow;
+             rewrite !Z.div_div, <-!Z.pow_add_r by (Core.zutil_arith || Z.zero_bounds); do 2 f_equal; nia).
         rewrite Z.div_between_0_if with (a:=x / 2^(k-1)) by (Z.zero_bounds; auto using q1_range).
         break_innermost_match; try lia; autorewrite with zsimplify_fast; [ | ].
         { apply partition_eq_mod; auto with zarith. }
@@ -437,6 +403,7 @@ Module Fancy.
              break_innermost_match; autorewrite with zsimplify; reflexivity).
         rewrite shiftr_correct by (rewrite ?Z.div_small, ?Z2Nat.inj_0 by lia; auto with zarith lia).
         autorewrite with weight_to_pow pull_Zpow pull_Zdiv.
+        rewrite !Z.div_div, <-!Z.pow_add_r by (Core.zutil_arith || Z.zero_bounds).
         congruence.
       Qed.
 
diff --git a/src/Arithmetic/BaseConversion.v b/src/Arithmetic/BaseConversion.v
index a22aa0c0b..c06dd3d71 100644
--- a/src/Arithmetic/BaseConversion.v
+++ b/src/Arithmetic/BaseConversion.v
@@ -1,66 +1,19 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
+Require Import Coq.ZArith.ZArith.
 Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Coq.Lists.List.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Partition.
+Require Import Crypto.Arithmetic.Saturated.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
+
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Local Open Scope Z_scope.
 
 Module BaseConversion.
-  Import Positional. Import Partition.
+  Import Positional.
   Section BaseConversion.
-    Hint Resolve Z.positive_is_nonzero Z.lt_gt Z.gt_lt.
     Context (sw dw : nat -> Z) (* source/destination weight functions *)
             {swprops : @weight_properties sw}
             {dwprops : @weight_properties dw}.
@@ -74,8 +27,8 @@ Module BaseConversion.
       eval dw dn (convert_bases sn dn p) = eval sw sn p.
     Proof using dwprops.
       cbv [convert_bases]; intros.
-      rewrite eval_chained_carries_no_reduce by auto.
-      rewrite eval_from_associational; auto.
+      rewrite eval_chained_carries_no_reduce by auto with zarith.
+      rewrite eval_from_associational; auto with zarith.
     Qed.
 
     Lemma length_convert_bases sn dn p
@@ -109,7 +62,7 @@ Module BaseConversion.
          @Associational.eval_mul
          @Positional.eval_to_associational
          Associational.eval_carryterm
-         @eval_convert_bases using solve [auto using Z.positive_is_nonzero] : push_eval.
+         @eval_convert_bases using solve [auto with zarith] : push_eval.
 
     Ltac push_eval := intros; autorewrite with push_eval; auto with zarith.
 
@@ -132,7 +85,7 @@ Module BaseConversion.
         autorewrite with push_fold_right. break_match; push_eval.
       Qed.
     End reorder.
-    Hint Rewrite eval_reordering_carry using solve [auto using Z.positive_is_nonzero] : push_eval.
+    Hint Rewrite eval_reordering_carry using solve [auto with zarith] : push_eval.
 
     (* carry at specified indices in dw, then use Rows.flatten to convert to Positional with sw *)
     Definition from_associational idxs n (p : list (Z * Z)) : list Z :=
@@ -257,8 +210,6 @@ Module BaseConversion.
     Local Notation deval := (Positional.eval dw).
     Local Notation seval := (Positional.eval sw).
 
-    Hint Resolve Z.gt_lt Z.positive_is_nonzero Nat2Z.is_nonneg.
-
     Definition widemul a b := mul_converted sw dw m m mn mn nout (aligned_carries n nout) a b.
 
     Lemma widemul_correct a b :
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 23b796d8a..91e63af9f 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -1,73 +1,28 @@
 (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.Structures.Orders.
 Require Import Coq.Lists.List.
 Require Import Crypto.Algebra.Nsatz.
+Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.Decidable.Bool2Prop.
+Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.UniquePose.
-
-Require Import Crypto.Util.Notations.
-  
-(*
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Zselect.
+Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
-*)
 Import ListNotations. Local Open Scope Z_scope.
 
 Module Associational.
diff --git a/src/Arithmetic/FancyMontgomeryReduction.v b/src/Arithmetic/FancyMontgomeryReduction.v
index 54b6ddd5f..258b2327e 100644
--- a/src/Arithmetic/FancyMontgomeryReduction.v
+++ b/src/Arithmetic/FancyMontgomeryReduction.v
@@ -1,61 +1,31 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
 Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Util.Notations.
+Require Import Coq.Lists.List.
+Require Import Crypto.Arithmetic.BaseConversion.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Partition.
+Require Import Crypto.Arithmetic.Saturated.
+Require Import Crypto.Arithmetic.UniformWeight.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
+Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
+Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
 Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
 Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+
+Require Import Crypto.Util.Notations.
+Import ListNotations. Local Open Scope Z_scope.
 
 Module MontgomeryReduction.
   Local Coercion Z.of_nat : nat >-> Z.
@@ -65,23 +35,23 @@ Module MontgomeryReduction.
             (N'_good : Z.equiv_modulo R (N*N') (-1)) (R'_good: Z.equiv_modulo N (R*R') 1).
 
     Context (Zlog2R : Z) .
-    Let w : nat -> Z := weight Zlog2R 1.
+    Let w : nat -> Z := uweight Zlog2R.
     Context (n:nat) (Hn_nz: n <> 0%nat) (n_good : Zlog2R mod Z.of_nat n = 0).
     Context (R_big_enough : 2 <= Zlog2R)
             (R_two_pow : 2^Zlog2R = R).
-    Let w_mul : nat -> Z := weight (Zlog2R / n) 1.
+    Let w_mul : nat -> Z := uweight (Zlog2R / n).
 
     Definition montred' (lo hi : Z) :=
       dlet_nd y := nth_default 0 (BaseConversion.widemul_inlined Zlog2R 1 2 [lo] [N']) 0  in
       dlet_nd t1_t2 := (BaseConversion.widemul_inlined_reverse Zlog2R 1 2 [N] [y]) in
-      dlet_nd sum_carry := Rows.add (weight Zlog2R 1) 2 [lo;hi] t1_t2 in
+      dlet_nd sum_carry := Rows.add w 2 [lo;hi] t1_t2 in
       dlet_nd y' := Z.zselect (snd sum_carry) 0 N in
       dlet_nd lo''_carry := Z.sub_get_borrow_full R (nth_default 0 (fst sum_carry) 1) y' in
       Z.add_modulo (fst lo''_carry) 0 N.
 
     Local Lemma Hw : forall i, w i = R ^ Z.of_nat i.
     Proof.
-      clear -R_big_enough R_two_pow; cbv [w weight]; intro.
+      clear -R_big_enough R_two_pow; cbv [w uweight weight]; intro.
       autorewrite with zsimplify.
       rewrite Z.pow_mul_r, R_two_pow by omega; reflexivity.
     Qed.
diff --git a/src/Arithmetic/Freeze.v b/src/Arithmetic/Freeze.v
new file mode 100644
index 000000000..d59812dea
--- /dev/null
+++ b/src/Arithmetic/Freeze.v
@@ -0,0 +1,352 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
+Require Import Crypto.Arithmetic.BaseConversion.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Saturated.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.ZUtil.EquivModulo.
+Require Import Crypto.Util.ZUtil.Opp.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+
+Require Import Crypto.Util.Notations.
+Local Open Scope Z_scope.
+
+(* TODO: rename this module? (Should it be, e.g., [Rows.freeze]?) *)
+Module Freeze.
+  Section Freeze.
+    Context weight {wprops : @weight_properties weight}.
+
+    Definition freeze n mask (m p:list Z) : list Z :=
+      let '(p, carry) := Rows.sub weight n p m in
+      let '(r, carry) := Rows.conditional_add weight n mask (-carry) p m in
+      r.
+
+    Lemma freezeZ m s c y :
+      m = s - c ->
+      0 < c < s ->
+      s <> 0 ->
+      0 <= y < 2*m ->
+      ((y - m) + (if (dec (-((y - m) / s) = 0)) then 0 else m)) mod s
+      = y mod m.
+    Proof using Type.
+      clear; intros.
+      transitivity ((y - m) mod m);
+        repeat first [ progress intros
+                     | progress subst
+                     | rewrite Z.opp_eq_0_iff in *
+                     | break_innermost_match_step
+                     | progress autorewrite with zsimplify_fast
+                     | rewrite Z.div_small_iff in * by auto
+                     | progress (Z.rewrite_mod_small; push_Zmod; Z.rewrite_mod_small)
+                     | progress destruct_head'_or
+                     | omega ].
+    Qed.
+
+    Lemma length_freeze n mask m p :
+      length m = n -> length p = n -> length (freeze n mask m p) = n.
+    Proof using wprops.
+      cbv [freeze Rows.conditional_add Rows.add]; eta_expand; intros.
+      distr_length; try assumption; cbn; intros; destruct_head'_or; destruct_head' False; subst;
+        distr_length.
+      erewrite Rows.length_sum_rows by (reflexivity || eassumption || distr_length); distr_length.
+    Qed.
+    Lemma eval_freeze_eq n mask m p
+          (n_nonzero:n<>0%nat)
+          (Hmask : List.map (Z.land mask) m = m)
+          (Hplen : length p = n)
+          (Hmlen : length m = n)
+      : Positional.eval weight n (@freeze n mask m p)
+        = (Positional.eval weight n p - Positional.eval weight n m +
+           (if dec (-((Positional.eval weight n p - Positional.eval weight n m) / weight n) = 0) then 0 else Positional.eval weight n m))
+            mod weight n.
+            (*if dec ((Positional.eval weight n p - Positional.eval weight n m) / weight n = 0)
+          then Positional.eval weight n p - Positional.eval weight n m
+          else Positional.eval weight n p mod weight n.*)
+    Proof using wprops.
+      pose proof (@weight_positive weight wprops n).
+      cbv [freeze Z.equiv_modulo]; eta_expand.
+      repeat first [ solve [auto]
+                   | rewrite Rows.conditional_add_partitions
+                   | rewrite Rows.sub_partitions
+                   | rewrite Rows.sub_div
+                   | rewrite Partition.eval_partition
+                   | progress distr_length
+                   | progress pull_Zmod (*
+                   | progress break_innermost_match_step
+                   | progress destruct_head'_or
+                   | omega
+                   | f_equal; omega
+                   | rewrite Z.div_small_iff in * by (auto using (@weight_positive weight ltac:(assumption)))
+                   | progress Z.rewrite_mod_small *) ].
+    Qed.
+
+    Lemma eval_freeze n c mask m p
+          (n_nonzero:n<>0%nat)
+          (Hc : 0 < Associational.eval c < weight n)
+          (Hmask : List.map (Z.land mask) m = m)
+          (modulus:=weight n - Associational.eval c)
+          (Hm : Positional.eval weight n m = modulus)
+          (Hp : 0 <= Positional.eval weight n p < 2*modulus)
+          (Hplen : length p = n)
+          (Hmlen : length m = n)
+      : Positional.eval weight n (@freeze n mask m p)
+        = Positional.eval weight n p mod modulus.
+    Proof using wprops.
+      pose proof (@weight_positive weight wprops n).
+      rewrite eval_freeze_eq by assumption.
+      erewrite freezeZ; try eassumption; try omega.
+      f_equal; omega.
+    Qed.
+
+    Lemma freeze_partitions n c mask m p
+          (n_nonzero:n<>0%nat)
+          (Hc : 0 < Associational.eval c < weight n)
+          (Hmask : List.map (Z.land mask) m = m)
+          (modulus:=weight n - Associational.eval c)
+          (Hm : Positional.eval weight n m = modulus)
+          (Hp : 0 <= Positional.eval weight n p < 2*modulus)
+          (Hplen : length p = n)
+          (Hmlen : length m = n)
+      : @freeze n mask m p = Partition.partition weight n (Positional.eval weight n p mod modulus).
+    Proof using wprops.
+      pose proof (@weight_positive weight wprops n).
+      pose proof (fun v => Z.mod_pos_bound v (weight n) ltac:(lia)).
+      pose proof (Z.mod_pos_bound (Positional.eval weight n p) modulus ltac:(lia)).
+      subst modulus.
+      erewrite <- eval_freeze by eassumption.
+      cbv [freeze]; eta_expand.
+      rewrite Rows.conditional_add_partitions by (auto; rewrite Rows.sub_partitions; auto; distr_length).
+      rewrite !Partition.eval_partition by assumption.
+      apply Partition.partition_Proper; [ assumption .. | ].
+      cbv [Z.equiv_modulo].
+      pull_Zmod; reflexivity.
+    Qed.
+  End Freeze.
+End Freeze.
+Hint Rewrite Freeze.length_freeze : distr_length.
+
+Section freeze_mod_ops.
+  Import Positional.
+  Import Freeze.
+  Local Coercion Z.of_nat : nat >-> Z.
+  Local Coercion QArith_base.inject_Z : Z >-> Q.
+  (* Design constraints:
+     - inputs must be [Z] (b/c reification does not support Q)
+     - internal structure must not match on the arguments (b/c reification does not support [positive]) *)
+  Context (limbwidth_num limbwidth_den : Z)
+          (limbwidth_good : 0 < limbwidth_den <= limbwidth_num)
+          (s : Z)
+          (c : list (Z*Z))
+          (n : nat)
+          (bitwidth : Z)
+          (m_enc : list Z)
+          (m_nz:s - Associational.eval c <> 0) (s_nz:s <> 0)
+          (Hn_nz : n <> 0%nat).
+  Local Notation bytes_weight := (@weight 8 1).
+  Local Notation weight := (@weight limbwidth_num limbwidth_den).
+  Let m := (s - Associational.eval c).
+
+  Context (Hs : s = weight n).
+  Context (c_small : 0 < Associational.eval c < weight n)
+          (m_enc_bounded : List.map (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc)
+          (m_enc_correct : Positional.eval weight n m_enc = m)
+          (Hm_enc_len : length m_enc = n).
+
+  Definition wprops_bytes := (@wprops 8 1 ltac:(clear; lia)).
+  Local Notation wprops := (@wprops limbwidth_num limbwidth_den limbwidth_good).
+
+  Local Notation wunique := (@weight_unique limbwidth_num limbwidth_den limbwidth_good).
+  Local Notation wunique_bytes := (@weight_unique 8 1 ltac:(clear; lia)).
+
+  Local Hint Immediate (wprops).
+  Local Hint Immediate (wprops_bytes).
+  Local Hint Immediate (weight_0 wprops).
+  Local Hint Immediate (weight_positive wprops).
+  Local Hint Immediate (weight_multiples wprops).
+  Local Hint Immediate (weight_divides wprops).
+  Local Hint Immediate (weight_0 wprops_bytes).
+  Local Hint Immediate (weight_positive wprops_bytes).
+  Local Hint Immediate (weight_multiples wprops_bytes).
+  Local Hint Immediate (weight_divides wprops_bytes).
+  Local Hint Immediate (wunique) (wunique_bytes).
+  Local Hint Resolve (wunique) (wunique_bytes).
+
+  Definition bytes_n
+    := Eval cbv [Qceiling Qdiv inject_Z Qfloor Qmult Qopp Qnum Qden Qinv Pos.mul]
+      in Z.to_nat (Qceiling (Z.log2_up (weight n) / 8)).
+
+  Lemma weight_bytes_weight_matches
+    : weight n <= bytes_weight bytes_n.
+  Proof using limbwidth_good.
+    clear -limbwidth_good.
+    cbv [weight bytes_n].
+    autorewrite with zsimplify_const.
+    rewrite Z.log2_up_pow2, !Z2Nat.id, !Z.opp_involutive by (Z.div_mod_to_quot_rem; nia).
+    Z.peel_le.
+    Z.div_mod_to_quot_rem; nia.
+  Qed.
+
+  Definition to_bytes (v : list Z)
+    := BaseConversion.convert_bases weight bytes_weight n bytes_n v.
+
+  Definition from_bytes (v : list Z)
+    := BaseConversion.convert_bases bytes_weight weight bytes_n n v.
+
+  Definition freeze_to_bytesmod (f : list Z) : list Z
+    := to_bytes (freeze weight n (Z.ones bitwidth) m_enc f).
+
+  Definition to_bytesmod (f : list Z) : list Z
+    := to_bytes f.
+
+  Definition from_bytesmod (f : list Z) : list Z
+    := from_bytes f.
+
+  Lemma bytes_nz : bytes_n <> 0%nat.
+  Proof using limbwidth_good Hn_nz.
+    clear -limbwidth_good Hn_nz.
+    cbv [bytes_n].
+    cbv [Qceiling Qdiv inject_Z Qfloor Qmult Qopp Qnum Qden Qinv].
+    autorewrite with zsimplify_const.
+    change (Z.pos (1*8)) with 8.
+    cbv [weight].
+    rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem; nia).
+    autorewrite with zsimplify_fast.
+    rewrite <- Z2Nat.inj_0, Z2Nat.inj_iff by (Z.div_mod_to_quot_rem; nia).
+    Z.div_mod_to_quot_rem; nia.
+  Qed.
+
+  Lemma bytes_n_big : weight n <= bytes_weight bytes_n.
+  Proof using limbwidth_good Hn_nz.
+    clear -limbwidth_good Hn_nz.
+    cbv [bytes_n bytes_weight].
+    Z.peel_le.
+    rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem; nia).
+    autorewrite with zsimplify_fast.
+    rewrite Z2Nat.id by (Z.div_mod_to_quot_rem; nia).
+    Z.div_mod_to_quot_rem; nia.
+  Qed.
+
+  Lemma eval_to_bytes
+    : forall (f : list Z)
+        (Hf : length f = n),
+      eval bytes_weight bytes_n (to_bytes f) = eval weight n f.
+  Proof using limbwidth_good Hn_nz.
+    generalize wprops wprops_bytes; clear -Hn_nz limbwidth_good.
+    intros.
+    cbv [to_bytes].
+    rewrite BaseConversion.eval_convert_bases
+      by (auto using bytes_nz; distr_length; auto using wprops).
+    reflexivity.
+  Qed.
+
+  Lemma to_bytes_partitions
+    : forall (f : list Z)
+             (Hf : length f = n)
+             (Hf_small : 0 <= eval weight n f < weight n),
+      to_bytes f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f).
+  Proof using Hn_nz limbwidth_good.
+    clear -Hn_nz limbwidth_good.
+    intros; cbv [to_bytes].
+    pose proof weight_bytes_weight_matches.
+    apply BaseConversion.convert_bases_partitions; eauto; lia.
+  Qed.
+
+  Lemma eval_to_bytesmod
+    : forall (f : list Z)
+             (Hf : length f = n)
+             (Hf_small : 0 <= eval weight n f < weight n),
+      eval bytes_weight bytes_n (to_bytesmod f) = eval weight n f
+      /\ to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f).
+  Proof using Hn_nz limbwidth_good.
+    split; apply eval_to_bytes || apply to_bytes_partitions; assumption.
+  Qed.
+
+  Lemma eval_freeze_to_bytesmod_and_partitions
+    : forall (f : list Z)
+        (Hf : length f = n)
+        (Hf_bounded : 0 <= eval weight n f < 2 * m),
+      (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m
+      /\ freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m).
+  Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    clear -m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    intros; subst m s.
+    cbv [freeze_to_bytesmod].
+    rewrite eval_to_bytes, to_bytes_partitions;
+      erewrite ?eval_freeze by eauto using wprops;
+      autorewrite with distr_length; eauto.
+    Z.div_mod_to_quot_rem; nia.
+  Qed.
+
+  Lemma eval_freeze_to_bytesmod
+    : forall (f : list Z)
+        (Hf : length f = n)
+        (Hf_bounded : 0 <= eval weight n f < 2 * m),
+      (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m.
+  Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    intros; now apply eval_freeze_to_bytesmod_and_partitions.
+  Qed.
+
+  Lemma freeze_to_bytesmod_partitions
+    : forall (f : list Z)
+        (Hf : length f = n)
+        (Hf_bounded : 0 <= eval weight n f < 2 * m),
+      freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m).
+  Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    intros; now apply eval_freeze_to_bytesmod_and_partitions.
+  Qed.
+
+  Lemma eval_from_bytes
+    : forall (f : list Z)
+        (Hf : length f = bytes_n),
+      eval weight n (from_bytes f) = eval bytes_weight bytes_n f.
+  Proof using limbwidth_good Hn_nz.
+    generalize wprops wprops_bytes; clear -Hn_nz limbwidth_good.
+    intros.
+    cbv [from_bytes].
+    rewrite BaseConversion.eval_convert_bases
+      by (auto using bytes_nz; distr_length; auto using wprops).
+    reflexivity.
+  Qed.
+
+  Lemma from_bytes_partitions
+    : forall (f : list Z)
+             (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
+      from_bytes f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+  Proof using limbwidth_good.
+    clear -limbwidth_good.
+    intros; cbv [from_bytes].
+    pose proof weight_bytes_weight_matches.
+    apply BaseConversion.convert_bases_partitions; eauto; lia.
+  Qed.
+
+  Lemma eval_from_bytesmod
+    : forall (f : list Z)
+             (Hf : length f = bytes_n),
+      eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f.
+  Proof using Hn_nz limbwidth_good. apply eval_from_bytes. Qed.
+
+  Lemma from_bytesmod_partitions
+    : forall (f : list Z)
+             (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
+      from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+  Proof using limbwidth_good. apply from_bytes_partitions. Qed.
+
+  Lemma eval_from_bytesmod_and_partitions
+    : forall (f : list Z)
+             (Hf : length f = bytes_n)
+             (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
+      eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f
+      /\ from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+  Proof using limbwidth_good Hn_nz.
+    now (split; [ apply eval_from_bytesmod | apply from_bytes_partitions ]).
+  Qed.
+End freeze_mod_ops.
+Hint Rewrite eval_freeze_to_bytesmod eval_to_bytes eval_to_bytesmod eval_from_bytes eval_from_bytesmod : push_eval.
\ No newline at end of file
diff --git a/src/Arithmetic/ModOps.v b/src/Arithmetic/ModOps.v
index 414c490aa..49f99f4fe 100644
--- a/src/Arithmetic/ModOps.v
+++ b/src/Arithmetic/ModOps.v
@@ -1,61 +1,13 @@
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
 Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
 Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section mod_ops.
   Import Positional.
diff --git a/src/Arithmetic/Partition.v b/src/Arithmetic/Partition.v
index 4c62124bf..2d2fb87fa 100644
--- a/src/Arithmetic/Partition.v
+++ b/src/Arithmetic/Partition.v
@@ -1,64 +1,13 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Structures.Orders.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
 
-Import Weight.
+Require Import Crypto.Util.Notations.
+Import ListNotations Weight. Local Open Scope Z_scope.
 
 Section Partition.
   Context weight {wprops : @weight_properties weight}.
@@ -82,8 +31,8 @@ Section Partition.
   Proof using wprops.
     induction n; intros.
     { cbn. rewrite (weight_0); auto with zarith. }
-    { rewrite (Z.div_mod (x mod weight (S n)) (weight n)) by auto.
-      rewrite <-Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto).
+    { rewrite (Z.div_mod (x mod weight (S n)) (weight n)) by auto with zarith.
+      rewrite <-Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto with zarith).
       rewrite partition_step, Positional.eval_snoc with (n:=n) by distr_length.
       omega. }
   Qed.
@@ -96,11 +45,11 @@ Section Partition.
     { reflexivity. }
     { assert (Hxyn : x mod weight n = y mod weight n).
       { erewrite (Znumtheory.Zmod_div_mod _ (weight (S n)) x), (Znumtheory.Zmod_div_mod _ (weight (S n)) y), Hxy
-          by (try apply Z.mod_divide; auto);
+          by (try apply Z.mod_divide; auto with zarith);
           reflexivity. }
       rewrite !partition_step, IHn by eauto.
-      rewrite (Z.div_mod (x mod weight (S n)) (weight n)), (Z.div_mod (y mod weight (S n)) (weight n)) by auto.
-      rewrite <-!Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto).
+      rewrite (Z.div_mod (x mod weight (S n)) (weight n)), (Z.div_mod (y mod weight (S n)) (weight n)) by auto with zarith.
+      rewrite <-!Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto with zarith).
       rewrite Hxy, Hxyn; reflexivity. }
   Qed.
 
@@ -135,8 +84,8 @@ Section Partition.
     pose proof (@weight_divides _ wprops j).
     f_equal;
       repeat match goal with
-             | _ => rewrite Z.mod_pull_div by auto using Z.lt_le_incl
-             | _ => rewrite weight_multiples by auto
+             | _ => rewrite Z.mod_pull_div by auto with zarith 
+             | _ => rewrite weight_multiples by auto with zarith
              | _ => progress autorewrite with zsimplify_fast zdiv_to_mod pull_Zdiv
              | _ => reflexivity
              end.
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index c0fe26a43..c82f6afa9 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -1,147 +1,109 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Crypto.Algebra.Ring.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.Partition.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 
-Module Saturated.
-  Module Associational.
-    Section Associational.
+Require Import Crypto.Util.Notations.
+Import ListNotations. Local Open Scope Z_scope.
 
-      Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) :=
-        dlet_nd xy := Z.mul_split s (snd t) (snd t') in
-              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].
+Module Associational.
+  Section Associational.
 
-      Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) :=
-        flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p.
+    Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) :=
+      dlet_nd xy := Z.mul_split s (snd t) (snd t') in
+      [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].
 
-      Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0):
-        Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q.
-      Proof using Type.
-        cbv [sat_multerm Let_In]; induction q;
-          repeat match goal with
-                 | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
-                 | _ => progress simpl flat_map
-                 | _ => rewrite IHq
-                 | _ => rewrite Z.mod_eq by assumption
-                 | _ => ring_simplify; omega
-                 end.
-      Qed.
-      Hint Rewrite eval_map_sat_multerm using (omega || assumption) : push_eval.
+    Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) :=
+      flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p.
 
-      Lemma eval_sat_mul s p q (s_nonzero:s<>0):
-        Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q.
-      Proof using Type.
-        cbv [sat_mul]; induction p; [reflexivity|].
+    Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0):
+      Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q.
+    Proof using Type.
+      cbv [sat_multerm Let_In]; induction q;
         repeat match goal with
-               | _ => progress (autorewrite with push_flat_map push_eval in * )
-               | _ => rewrite IHp
+               | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
+               | _ => progress simpl flat_map
+               | _ => rewrite IHq
+               | _ => rewrite Z.mod_eq by assumption
                | _ => ring_simplify; omega
                end.
-      Qed.
-      Hint Rewrite eval_sat_mul : push_eval.
-
-      Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) :=
-        if snd t =? 1
-        then [(fst t * fst t', snd t')]
-        else if snd t =? -1
-             then [(fst t * fst t', - snd t')]
-             else if snd t =? 0
-                  then nil
-                  else dlet_nd xy := Z.mul_split s (snd t) (snd t') in
-              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].
-
-      Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) :=
-        flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p.
-
-      Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0):
-        Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q.
-      Proof using Type.
-        cbv [sat_multerm_const Let_In]; induction q;
-          repeat match goal with
-                 | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
-                 | _ => progress simpl flat_map
-                 | H : _ = 1 |- _ => rewrite H
-                 | H : _ = -1 |- _ => rewrite H
-                 | H : _ = 0 |- _ => rewrite H
-                 | _ => progress break_match; Z.ltb_to_lt
-                 | _ => rewrite IHq
-                 | _ => rewrite Z.mod_eq by assumption
-                 | _ => ring_simplify; omega
-                 end.
-      Qed.
-      Hint Rewrite eval_map_sat_multerm_const using (omega || assumption) : push_eval.
+    Qed.
+    Hint Rewrite eval_map_sat_multerm using (omega || assumption) : push_eval.
 
-      Lemma eval_sat_mul_const s p q (s_nonzero:s<>0):
-        Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q.
-      Proof using Type.
-        cbv [sat_mul_const]; induction p; [reflexivity|].
+    Lemma eval_sat_mul s p q (s_nonzero:s<>0):
+      Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q.
+    Proof using Type.
+      cbv [sat_mul]; induction p; [reflexivity|].
+      repeat match goal with
+             | _ => progress (autorewrite with push_flat_map push_eval in * )
+             | _ => rewrite IHp
+             | _ => ring_simplify; omega
+             end.
+    Qed.
+    Hint Rewrite eval_sat_mul : push_eval.
+
+    Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) :=
+      if snd t =? 1
+      then [(fst t * fst t', snd t')]
+      else if snd t =? -1
+           then [(fst t * fst t', - snd t')]
+           else if snd t =? 0
+                then nil
+                else dlet_nd xy := Z.mul_split s (snd t) (snd t') in
+            [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].
+
+    Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) :=
+      flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p.
+
+    Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0):
+      Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q.
+    Proof using Type.
+      cbv [sat_multerm_const Let_In]; induction q;
         repeat match goal with
-               | _ => progress (autorewrite with push_flat_map push_eval in * )
-               | _ => rewrite IHp
+               | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
+               | _ => progress simpl flat_map
+               | H : _ = 1 |- _ => rewrite H
+               | H : _ = -1 |- _ => rewrite H
+               | H : _ = 0 |- _ => rewrite H
+               | _ => progress break_match; Z.ltb_to_lt
+               | _ => rewrite IHq
+               | _ => rewrite Z.mod_eq by assumption
                | _ => ring_simplify; omega
                end.
-      Qed.
-      Hint Rewrite eval_sat_mul_const : push_eval.
-    End Associational.
+    Qed.
+    Hint Rewrite eval_map_sat_multerm_const using (omega || assumption) : push_eval.
+
+    Lemma eval_sat_mul_const s p q (s_nonzero:s<>0):
+      Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q.
+    Proof using Type.
+      cbv [sat_mul_const]; induction p; [reflexivity|].
+      repeat match goal with
+             | _ => progress (autorewrite with push_flat_map push_eval in * )
+             | _ => rewrite IHp
+             | _ => ring_simplify; omega
+             end.
+    Qed.
+    Hint Rewrite eval_sat_mul_const : push_eval.
   End Associational.
-End Saturated.
+End Associational.
 
 Module Columns.
-  Import Saturated. Import Partition. Import Weight.
+  Import Weight.
   Section Columns.
     Context weight {wprops : @weight_properties weight}.
 
@@ -375,10 +337,9 @@ Module Columns.
 End Columns.
 
 Module Rows.
-  Import Saturated. Import Partition. Import Weight.
+  Import Weight.
   Section Rows.
     Context weight {wprops : @weight_properties weight}.
-    Hint Resolve Z.positive_is_nonzero Z.lt_gt.
     Local Notation rows := (list (list Z)) (only parsing).
     Local Notation cols := (list (list Z)) (only parsing).
 
@@ -714,7 +675,7 @@ Module Rows.
                    | _ => rewrite partition_step by auto
                    | _ => rewrite weight_div_pull_div by auto
                    | _ => rewrite weight_mod_pull_div by auto
-                   | _ => rewrite <-Z.div_add' by auto
+                   | _ => rewrite <-Z.div_add' by auto with zarith
                    | _ => progress push
                    end.
           f_equal; push; [ ].
@@ -802,9 +763,9 @@ Module Rows.
                  | _ => rewrite IHinp by push; clear IHinp
                  | |- pair _ _ = pair _ _ => f_equal
                  | _ => apply (@partition_eq_mod _ wprops)
-                 | _ => rewrite <-Z.div_add_l' by auto
+                 | _ => rewrite <-Z.div_add_l' by auto with zarith
                  | _ => rewrite Z.mod_add'_full by omega
-                 | _ => rewrite Z.mul_div_eq_full by auto
+                 | _ => rewrite Z.mul_div_eq_full by auto with zarith
                  | _ => progress (push_Zmod; pull_Zmod)
                  | _ => progress push
                  end.
@@ -980,7 +941,7 @@ Module Rows.
         rewrite Z.div_sub_small, Z.ltb_antisym by omega.
         destruct (Positional.eval weight n q <=? Positional.eval weight n p);
           cbn [negb]; autorewrite with zsimplify_fast;
-            break_match; congruence.
+            break_match; try lia; congruence.
       Qed.
 
       Let sub_then_maybe_add_Z a b c :=
@@ -1028,7 +989,7 @@ Module Rows.
         cbv [adjust_s]; rewrite fold_right_map; generalize (List.rev (seq 0 fuel)); intro ls; induction ls as [|l ls IHls];
           cbn.
         { rewrite Z.mod_same by assumption; auto. }
-        { break_match; cbn in *; auto. }
+        { break_match; cbn in *; auto with zarith. }
       Qed.
 
       Lemma eval_sat_reduce base s c n p :
@@ -1064,7 +1025,7 @@ Module Rows.
       Proof using wprops.
         solver. cbn [fst snd].
         rewrite eval_partition by auto.
-        rewrite <-Z.div_mod'' by auto.
+        rewrite <-Z.div_mod'' by auto with zarith.
         autorewrite with push_eval; reflexivity.
       Qed.
 
diff --git a/src/Arithmetic/UniformWeight.v b/src/Arithmetic/UniformWeight.v
index b880f384e..9af083994 100644
--- a/src/Arithmetic/UniformWeight.v
+++ b/src/Arithmetic/UniformWeight.v
@@ -1,61 +1,18 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
-Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Partition.
+Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+
+Require Import Crypto.Util.Notations.
+Local Open Scope Z_scope.
+Import Weight.
 
 Definition uweight (lgr : Z) : nat -> Z
   := weight lgr 1.
@@ -76,14 +33,14 @@ Proof using Type.
   rewrite !Positional.eval_snoc with (n:=n) by distr_length.
   rewrite IHxs, !uweight_eq_alt by omega.
   autorewrite with push_Zof_nat push_Zpow.
-  rewrite !Z.pow_succ_r by auto using Nat2Z.is_nonneg.
+  rewrite !Z.pow_succ_r by auto with zarith.
   ring.
 Qed.
 Lemma uweight_S lgr (Hr : 0 <= lgr) n : uweight lgr (S n) = 2 ^ lgr * uweight lgr n.
 Proof using Type.
   rewrite !uweight_eq_alt by auto.
   autorewrite with push_Zof_nat.
-  rewrite Z.pow_succ_r by auto using Nat2Z.is_nonneg.
+  rewrite Z.pow_succ_r by auto with zarith.
   reflexivity.
 Qed.
 Lemma uweight_double_le lgr (Hr : 0 < lgr) n : uweight lgr n + uweight lgr n <= uweight lgr (S n).
diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v
index f52dbdeb1..2477d212e 100644
--- a/src/Arithmetic/WordByWordMontgomery.v
+++ b/src/Arithmetic/WordByWordMontgomery.v
@@ -1,65 +1,36 @@
-
-(* TODO: prune these *)
-Require Import Crypto.Algebra.Nsatz.
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Coq.Sorting.Mergesort Coq.Structures.Orders.
-Require Import Coq.Sorting.Permutation.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *)
-Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *)
-Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
-Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
-Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
-Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
-Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Crypto.Algebra.Ring.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.Freeze.
 Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
+Require Import Crypto.Arithmetic.Partition.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.RunTacticAsConstr.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.OptionList.
+Require Import Crypto.Arithmetic.Saturated.
+Require Import Crypto.Arithmetic.UniformWeight.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Sum.
-Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Sigma.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
-Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Modulo.PullPush.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Le.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Require Import Crypto.Util.Tactics.SetEvars.
+Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.SubstEvars.
+
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Sorting.
-Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
-Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
-Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Hints.PullPush.
-Require Import Crypto.Util.ZUtil.EquivModulo.
-Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Equality.
-Require Import Crypto.Util.Tactics.SetEvars.
-Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
+Import ListNotations. Local Open Scope Z_scope.
 
 Module WordByWordMontgomery.
-  Import Partition.
-  Local Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg.
   Section with_args.
     Context (lgr : Z)
             (m : Z).
@@ -201,14 +172,14 @@ Module WordByWordMontgomery.
       auto with zarith.
     Qed.
 
-    Let partition_Proper := (@partition_Proper _ wprops).
+    Let partition_Proper := (@Partition.partition_Proper _ wprops).
     Local Existing Instance partition_Proper.
     Lemma eval_nonzero n A : @small n A -> nonzero A = 0 <-> @eval n A = 0.
     Proof using lgr_big.
       clear -lgr_big partition_Proper.
       cbv [nonzero eval small]; intro Heq.
       do 2 rewrite Heq.
-      rewrite !eval_partition, Z.mod_mod by auto.
+      rewrite !eval_partition, Z.mod_mod by auto with zarith.
       generalize (Positional.eval weight n A); clear Heq A.
       induction n as [|n IHn].
       { cbn; rewrite weight_0 by auto; intros; autorewrite with zsimplify_const; omega. }
@@ -229,7 +200,7 @@ Module WordByWordMontgomery.
           rewrite <- !Z.mul_add_distr_l, Z.mul_eq_0.
           nia. }
         rewrite Heq at 1; rewrite IHn.
-        rewrite Z.mod_mod by auto.
+        rewrite Z.mod_mod by auto with zarith.
         generalize (weight_multiples ltac:(auto) n).
         generalize (weight_positive ltac:(auto) n).
         generalize (weight_positive ltac:(auto) (S n)).