Merged changes, including new ZUtil conventions.

17 files changed, 1198 insertions, 459 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index eca1b2bb1..62b216b92 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -711,36 +711,26 @@ Ltac deduplicate_nonfraction_pieces mul :=
            => subst x0 x1
          end.
 
-Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont :=
+Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div cont :=
   idtac;
   let one_arg_recr :=
       fun op v
       => set_nonfraction_pieces_on
-           v eq zero opp add sub mul inv div nonzero_tac
+           v eq zero opp add sub mul inv div
            ltac:(fun x => cont (op x)) in
   let two_arg_recr :=
       fun op v0 v1
       => set_nonfraction_pieces_on
-           v0 eq zero opp add sub mul inv div nonzero_tac
+           v0 eq zero opp add sub mul inv div
            ltac:(fun x
                  =>
                    set_nonfraction_pieces_on
-                     v1 eq zero opp add sub mul inv div nonzero_tac
+                     v1 eq zero opp add sub mul inv div
                      ltac:(fun y => cont (op x y))) in
   lazymatch T with
   | eq ?x ?y => two_arg_recr eq x y
   | appcontext[div]
     => lazymatch T with
-       | div ?numerator ?denominator
-         => let d := fresh "d" in
-            pose denominator as d;
-            cut (not (eq d zero));
-            [ intro;
-              set_nonfraction_pieces_on
-                numerator eq zero opp add sub mul inv div nonzero_tac
-                ltac:(fun numerator'
-                      => cont (div numerator' d))
-            | subst d; nonzero_tac ]
        | opp ?x => one_arg_recr opp x
        | inv ?x => one_arg_recr inv x
        | add ?x ?y => two_arg_recr add x y
@@ -753,32 +743,32 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con
          pose T as x;
          cont x
   end.
-Ltac set_nonfraction_pieces_in_by H nonzero_tac :=
+Ltac set_nonfraction_pieces_in H :=
   idtac;
   let fld := guess_field in
   lazymatch type of fld with
   | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
     => let T := type of H in
        set_nonfraction_pieces_on
-         T eq zero opp add sub mul inv div nonzero_tac
+         T eq zero opp add sub mul inv div
          ltac:(fun T' => change T' in H);
        deduplicate_nonfraction_pieces mul
   end.
-Ltac set_nonfraction_pieces_by nonzero_tac :=
+Ltac set_nonfraction_pieces :=
   idtac;
   let fld := guess_field in
   lazymatch type of fld with
   | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
     => let T := get_goal in
        set_nonfraction_pieces_on
-         T eq zero opp add sub mul inv div nonzero_tac
+         T eq zero opp add sub mul inv div
          ltac:(fun T' => change T');
        deduplicate_nonfraction_pieces mul
   end.
-Ltac set_nonfraction_pieces_in H :=
-  set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)).
-Ltac set_nonfraction_pieces :=
-  set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)).
+Ltac default_conservative_common_denominator_nonzero_tac :=
+  repeat apply conj;
+  try first [ assumption
+            | intro; field_nonzero_mul_split; tauto ].
 Ltac conservative_common_denominator_in H :=
   idtac;
   let fld := guess_field in
@@ -789,10 +779,9 @@ Ltac conservative_common_denominator_in H :=
   lazymatch type of H with
   | appcontext[div]
     => set_nonfraction_pieces_in H;
-       [ common_denominator_in H;
-         [
-         | repeat apply conj; try assumption.. ]
-       | .. ];
+       common_denominator_in H;
+       [
+       | default_conservative_common_denominator_nonzero_tac.. ];
        repeat match goal with H := _ |- _ => subst H end
   | ?T => fail 0 "no division in" H ":" T
   end.
@@ -806,10 +795,9 @@ Ltac conservative_common_denominator :=
   lazymatch goal with
   | |- appcontext[div]
     => set_nonfraction_pieces;
-       [ common_denominator;
-         [
-         | repeat apply conj; try assumption.. ]
-       | .. ];
+       common_denominator;
+       [
+       | default_conservative_common_denominator_nonzero_tac.. ];
        repeat match goal with H := _ |- _ => subst H end
   | |- ?G
     => fail 0 "no division in goal" G
@@ -846,14 +834,30 @@ Ltac conservative_common_denominator_inequality :=
   | let HG := fresh in
     intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ].
 
+Ltac conservative_common_denominator_hyps :=
+  try match goal with
+      | [H: _ |- _ ]
+        => progress conservative_common_denominator_in H;
+           [ conservative_common_denominator_hyps
+           | .. ]
+      end.
+
+Ltac conservative_common_denominator_inequality_hyps :=
+  try match goal with
+      | [H: _ |- _ ]
+        => progress conservative_common_denominator_inequality_in H;
+           [ conservative_common_denominator_inequality_hyps
+           | .. ]
+      end.
+
 Ltac conservative_common_denominator_all :=
   try conservative_common_denominator;
-  [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end
+  [ try conservative_common_denominator_hyps
   | .. ].
 
 Ltac conservative_common_denominator_inequality_all :=
   try conservative_common_denominator_inequality;
-  [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_inequality_in H; [] end
+  [ try conservative_common_denominator_inequality_hyps
   | .. ].
 
 Ltac conservative_common_denominator_equality_inequality_all :=
@@ -878,19 +882,41 @@ Ltac field_simplify_eq_hyps :=
 
 Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
 
-(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R] *)
+(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R], and similarly for symmetric relations *)
 Ltac clear_algebraic_duplicates_step R :=
   match goal with
   | [ H : R ?x ?x |- _ ]
     => clear H
   end.
+Ltac clear_algebraic_duplicates_step_S R :=
+  match goal with
+  | [ H : R ?x ?y, H' : R ?y ?x |- _ ]
+    => clear H
+  | [ H : not (R ?x ?y), H' : not (R ?y ?x) |- _ ]
+    => clear H
+  | [ H : (R ?x ?y -> False)%type, H' : (R ?y ?x -> False)%type |- _ ]
+    => clear H
+  | [ H : not (R ?x ?y), H' : (R ?y ?x -> False)%type |- _ ]
+    => clear H
+  end.
 Ltac clear_algebraic_duplicates_guarded R :=
   let test_reflexive := constr:(_ : Reflexive R) in
   repeat clear_algebraic_duplicates_step R.
+Ltac clear_algebraic_duplicates_guarded_S R :=
+  let test_symmetric := constr:(_ : Symmetric R) in
+  repeat clear_algebraic_duplicates_step_S R.
 Ltac clear_algebraic_duplicates :=
   clear_duplicates;
   repeat match goal with
-         | [ H : ?R ?x ?x |- _ ] => clear_algebraic_duplicates_guarded R
+         | [ H : ?R ?x ?x |- _ ] => progress clear_algebraic_duplicates_guarded R
+         | [ H : ?R ?x ?y, H' : ?R ?y ?x |- _ ]
+           => progress clear_algebraic_duplicates_guarded_S R
+         | [ H : not (?R ?x ?y), H' : not (?R ?y ?x) |- _ ]
+           => progress clear_algebraic_duplicates_guarded_S R
+         | [ H : not (?R ?x ?y), H' : (?R ?y ?x -> False)%type |- _ ]
+           => progress clear_algebraic_duplicates_guarded_S R
+         | [ H : (?R ?x ?y -> False)%type, H' : (?R ?y ?x -> False)%type |- _ ]
+           => progress clear_algebraic_duplicates_guarded_S R
          end.
 
 (*** Inequalities over fields *)
@@ -1006,16 +1032,43 @@ Ltac nsatz_inequality_to_equality :=
   | [ H : not (?R ?x ?zero) |- False ] => apply H
   | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H
   end.
+(** Clean up tactic handling side-conditions *)
+Ltac super_nsatz_post_clean_inequalities :=
+  repeat (apply conj || split_field_inequalities);
+  try assumption;
+  prensatz_contradict; nsatz_inequality_to_equality;
+  try nsatz.
+Ltac nsatz_equality_to_inequality_by_decide_equality :=
+  lazymatch goal with
+  | [ H : not (?R _ _) |- ?R _ _ ] => idtac
+  | [ H : (?R _ _ -> False)%type |- ?R _ _ ] => idtac
+  | [ |- ?R _ _ ] => fail 0 "No hypothesis exists which negates the relation" R
+  | [ |- ?G ] => fail 0 "The goal is not a binary relation:" G
+  end;
+  lazymatch goal with
+  | [ |- ?R ?x ?y ]
+    => destruct (@dec (R x y) _); [ assumption | exfalso ]
+  end.
 (** Handles inequalities and fractions *)
-Ltac super_nsatz :=
+Ltac super_nsatz_internal nsatz_alternative :=
   (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *)
   clear_algebraic_duplicates;
   prensatz_contradict;
   (* Each goal left over by [prensatz_contradict] is separate (and
      there might not be any), so we handle them all separately *)
   [ try conservative_common_denominator_equality_inequality_all;
-    [ try nsatz_inequality_to_equality; try nsatz
-    | repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; try nsatz.. ].. ].
+    [ try nsatz_inequality_to_equality;
+      try first [ nsatz;
+                  (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *)
+                  try super_nsatz_post_clean_inequalities
+                | nsatz_alternative ]
+    | super_nsatz_post_clean_inequalities.. ].. ].
+
+Ltac super_nsatz :=
+  super_nsatz_internal
+    (* if [nsatz] fails, we try turning the goal equality into an inequality and trying again *)
+    ltac:(nsatz_equality_to_inequality_by_decide_equality;
+          super_nsatz_internal idtac).
 
 Section ExtraLemmas.
   Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
@@ -1023,13 +1076,11 @@ Section ExtraLemmas.
   Local Notation "0" := zero. Local Notation "1" := one.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
 
+  Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y.
+  Proof. intros; super_nsatz. Qed.
+
   Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False.
-  Proof.
-    intros.
-    canonicalize_field_equalities; canonicalize_field_inequalities.
-    assert (H' : (x + y) * (x - y) <> 0) by (apply mul_nonzero_nonzero; assumption).
-    apply H'; nsatz.
-  Qed.
+  Proof. intros; super_nsatz. Qed.
 
   Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False.
   Proof.
@@ -1051,17 +1102,37 @@ Section ExtraLemmas.
 End ExtraLemmas.
 
 (** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *)
-Ltac pose_proof_only_two_square_roots x y H :=
+Ltac pose_proof_only_two_square_roots x y H eq opp mul :=
   not constr_eq x y;
-  match goal with
-  | [ H' : ?eq (?mul x x) (?mul y y) |- _ ]
-    => pose proof (only_two_square_roots'_choice x y H') as H
-  | [ H0 : ?eq (?mul x x) ?z, H1 : ?eq (?mul y y) ?z |- _ ]
-    => pose proof (only_two_square_roots_choice x y z H0 H1) as H
+  lazymatch x with
+  | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul
+  | _
+    => lazymatch y with
+       | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul
+       | _
+         => match goal with
+            | [ H' : eq x y |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq y x |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq x (opp y) |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq y (opp x) |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq (opp x) y |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq (opp y) x |- _ ]
+              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
+            | [ H' : eq (mul x x) (mul y y) |- _ ]
+              => pose proof (only_two_square_roots'_choice x y H') as H
+            | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ]
+              => pose proof (only_two_square_roots_choice x y z H0 H1) as H
+            end
+       end
   end.
-Ltac reduce_only_two_square_roots x y :=
+Ltac reduce_only_two_square_roots x y eq opp mul :=
   let H := fresh in
-  pose_proof_only_two_square_roots x y H;
+  pose_proof_only_two_square_roots x y H eq opp mul;
   destruct H;
   try setoid_subst y.
 Ltac pre_clean_only_two_square_roots :=
@@ -1075,21 +1146,25 @@ Ltac post_clean_only_two_square_roots x y :=
        | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity
        end);
   try setoid_subst x; try setoid_subst y.
-Ltac only_two_square_roots_step :=
+Ltac only_two_square_roots_step eq opp mul :=
   match goal with
-  | [ H : not (?eq ?x (?opp ?y)) |- _ ]
+  | [ H : not (eq ?x (opp ?y)) |- _ ]
     (* this one comes first, because it the procedure is asymmetric
        with respect to [x] and [y], and this order is more likely to
        lead to solving goals by contradiction. *)
-    => is_var x; is_var y; reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
-  | [ H : ?eq (?mul ?x ?x) (?mul ?y ?y) |- _ ]
-    => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
-  | [ H : ?eq (?mul ?x ?x) ?z, H' : ?eq (?mul ?y ?y) ?z |- _ ]
-    => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+    => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
+  | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ]
+    => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
+  | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ]
+    => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
   end.
 Ltac only_two_square_roots :=
   pre_clean_only_two_square_roots;
-  repeat only_two_square_roots_step.
+  let fld := guess_field in
+  lazymatch type of fld with
+  | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
+    => repeat only_two_square_roots_step eq opp mul
+  end.
 
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index a37932de0..0ad6c0a03 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -120,7 +120,7 @@ Section PolynomialBaseCoefs.
     rewrite in_map_iff in *.
     destruct H; destruct H.
     subst.
-    apply pos_pow_nat_pos.
+    apply Z.pos_pow_nat_pos.
   Qed.
 
   Lemma poly_base_defn : forall i, (i < length poly_base)%nat ->
@@ -145,7 +145,6 @@ Section PolynomialBaseCoefs.
       with (Z.pos b1); auto.
     rewrite Z_div_mult_full; auto.
     apply Z.pow_nonzero; intuition.
-    pose proof (Zgt_pos_0 b1); omega.
   Qed.
 
   Lemma poly_base_good:
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index a0372c60b..eb7f31ba6 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -84,7 +84,7 @@ Section BaseSystemProofs.
     intros.
     rewrite nth_default_eq.
     destruct (nth_in_or_default i base d).
-    + auto using positive_is_nonzero, base_positive.
+    + auto using Z.positive_is_nonzero, base_positive.
     + congruence.
   Qed.
 
@@ -94,7 +94,7 @@ Section BaseSystemProofs.
     intros.
     rewrite nth_default_eq.
     destruct (nth_in_or_default i base d).
-    + rewrite <-gt_lt_symmetry; auto using base_positive.
+    + apply Z.gt_lt; auto using base_positive.
     + congruence.
   Qed.
 
@@ -191,7 +191,7 @@ Section BaseSystemProofs.
   Lemma nth_error_base_nonzero : forall n x,
     nth_error base n = Some x -> x <> 0.
   Proof.
-    eauto using (@nth_error_value_In Z), Zgt0_neq0, base_positive.
+    eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive.
   Qed.
 
   Hint Rewrite plus_0_r.
@@ -594,7 +594,7 @@ Section BaseSystemProofs.
         specialize (H1 i H2);
         rewrite (Znumtheory.Zmod_div_mod _ _ _ (nth_default_base_pos _ H _)
                                                (nth_default_base_pos _ H _) H0) end.
-      rewrite <-Z.div_mod by (apply positive_is_nonzero, gt_lt_symmetry; auto using nth_default_base_pos).
+      rewrite <-Z.div_mod by (apply Z.positive_is_nonzero, Z.lt_gt; auto using nth_default_base_pos).
       reflexivity.
   Qed.
 
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index 41b75e216..033e99665 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -43,12 +43,12 @@ Section SignBit.
     pose proof (F_opp_spec x) as opp_spec_x.
     apply F_eq in opp_spec_x.
     rewrite FieldToZ_add in opp_spec_x.
-    rewrite <-opp_spec_x, Z_odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega).
-    replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega).
+    rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega).
+    replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega).
     rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega.
     apply Bool.xorb_eq.
     rewrite <-Bool.negb_xorb_l.
     assumption.
   Qed.
 
-End SignBit.
\ No newline at end of file
+End SignBit.
diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v
new file mode 100644
index 000000000..8b472d5d8
--- /dev/null
+++ b/src/ModularArithmetic/BarrettReduction/Z.v
@@ -0,0 +1,118 @@
+(*** 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 Crypto.Util.Tactics.
+
+Local Open Scope Z_scope.
+
+Section barrett.
+  Context (n a : Z)
+          (n_reasonable : n <> 0).
+  (** Quoting Wikipedia <https://en.wikipedia.org/wiki/Barrett_reduction>: *)
+  (** In modular arithmetic, Barrett reduction is a reduction
+      algorithm introduced in 1986 by P.D. Barrett. A naive way of
+      computing *)
+  (** [c = a mod n] *)
+  (** would be to use a fast division algorithm. Barrett reduction is
+      an algorithm designed to optimize this operation assuming [n] is
+      constant, and [a < n²], replacing divisions by
+      multiplications. *)
+
+  (** * General idea *)
+  Section general_idea.
+    (** Let [m = 1 / n] be the inverse of [n] as a floating point
+        number. Then *)
+    (** [a mod n = a - ⌊a m⌋ n] *)
+    (** where [⌊ x ⌋] denotes the floor function. The result is exact,
+        as long as [m] is computed with sufficient accuracy. *)
+
+    (* [/] is [Z.div], which means truncated division *)
+    Local Notation "⌊am⌋" := (a / n) (only parsing).
+
+    Theorem naive_barrett_reduction_correct
+      : a mod n = a - ⌊am⌋ * n.
+    Proof.
+      apply Zmod_eq_full; assumption.
+    Qed.
+  End general_idea.
+
+  (** * Barrett algorithm *)
+  Section barrett_algorithm.
+    (** Barrett algorithm is a fixed-point analog which expresses
+        everything in terms of integers. Let [k] be the smallest
+        integer such that [2ᵏ > n]. Think of [n] as representing the
+        fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m =
+        ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number
+        [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *)
+    (** N.B. We don't need [k] to be the smallest such integer. *)
+    Context (k : Z)
+            (k_good : n < 2 ^ k)
+            (m : Z)
+            (m_good : m = 4^k / n). (* [/] is [Z.div], which is truncated *)
+    (** Wikipedia neglects to mention non-negativity, but we need it.
+        It might be possible to do with a relaxed assumption, such as
+        the sign of [a] and the sign of [n] being the same; but I
+        figured it wasn't worth it. *)
+    Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *)
+            (a_nonneg : 0 <= a).
+
+    Lemma k_nonnegative : 0 <= k.
+    Proof.
+      destruct (Z_lt_le_dec k 0); try assumption.
+      rewrite !Z.pow_neg_r in * by lia; lia.
+    Qed.
+
+    (** Now *)
+    Let q := (m * a) / 4^k.
+    Let r := a - q * n.
+    (** Because of the floor function (in Coq, because [/] means
+        truncated division), [q] is an integer and [r ≡ a mod n]. *)
+    Theorem barrett_reduction_equivalent
+      : r mod n = a mod n.
+    Proof.
+      subst r q m.
+      rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption.
+      reflexivity.
+    Qed.
+
+    Lemma qn_small
+      : q * n <= a.
+    Proof.
+      pose proof k_nonnegative; subst q r m.
+      assert (0 <= 2^(k-1)) by zero_bounds.
+      Z.simplify_fractions_le.
+    Qed.
+
+    (** Also, if [a < n²] then [r < 2n]. *)
+    (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *)
+    Context (a_small : a < 4^k).
+    Lemma r_small : r < 2 * n.
+    Proof.
+      Hint Rewrite (Z.div_small a (4^k)) (Z.mod_small a (4^k)) using lia : zsimplify.
+      Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div.
+      cut (r + 1 <= 2 * n); [ lia | ].
+      pose proof k_nonnegative; subst r q m.
+      assert (0 <= 2^(k-1)) by zero_bounds.
+      assert (4^k <> 0) by auto with zarith lia.
+      assert (a mod n < n) by auto with zarith lia.
+      pose proof (Z.mod_pos_bound (a * 4^k / n) (4^k)).
+      transitivity (a - (a * 4 ^ k / n - a) / 4 ^ k * n + 1).
+      { rewrite <- (Z.mul_comm a); auto 6 with zarith lia. }
+      rewrite (Z_div_mod_eq (_ * 4^k / n) (4^k)) by lia.
+      autorewrite with push_Zmul push_Zopp zsimplify zstrip_div.
+      break_match; auto with lia.
+    Qed.
+
+    (** In that case, we have *)
+    Theorem barrett_reduction_small
+      : a mod n = if r <? n
+                  then r
+                  else r - n.
+    Proof.
+      pose proof r_small. pose proof qn_small.
+      destruct (r <? n) eqn:rlt; Z.ltb_to_lt.
+      { symmetry; apply (Zmod_unique a n q); subst r; lia. }
+      { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. }
+    Qed.
+  End barrett_algorithm.
+End barrett.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index bb9b1674e..ce11b157b 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -22,7 +22,7 @@ Definition Z_div_opt := Eval compute in Z.div.
 Definition Z_pow_opt := Eval compute in Z.pow.
 Definition Z_opp_opt := Eval compute in Z.opp.
 Definition Z_shiftl_opt := Eval compute in Z.shiftl.
-Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by.
+Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by.
 
 Definition nth_default_opt {A} := Eval compute in @nth_default A.
 Definition set_nth_opt {A} := Eval compute in @set_nth A.
@@ -502,11 +502,11 @@ Section Multiplication.
     cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce].
     rewrite <- mul'_opt_correct.
     change @base with base_opt.
-    rewrite map_shiftl by apply k_nonneg.
+    rewrite Z.map_shiftl by apply k_nonneg.
     rewrite c_subst.
     rewrite k_subst.
     change @map with @map_opt.
-    change @Z_shiftl_by with @Z_shiftl_by_opt.
+    change @Z.shiftl_by with @Z_shiftl_by_opt.
     reflexivity.
   Defined.
 
@@ -671,4 +671,4 @@ Section Canonicalization.
     auto using freeze_opt_preserves_rep.
   Qed.
 
-End Canonicalization.
\ No newline at end of file
+End Canonicalization.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 75806f570..29612d900 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -170,7 +170,7 @@ Section PseudoMersenneProofs.
     rewrite Z.sub_sub_distr, Z.sub_diag.
     simpl.
     rewrite Z.mul_comm.
-    rewrite mod_mult_plus; auto using modulus_nonzero.
+    rewrite Z.mod_add_l; auto using modulus_nonzero.
     rewrite <- Zplus_mod; auto.
   Qed.
 
@@ -390,8 +390,8 @@ Section CarryProofs.
     rewrite nth_default_base_succ by omega.
     rewrite Z.mul_assoc.
     rewrite (Z.mul_comm _ (2 ^ log_cap i)).
-    rewrite mul_div_eq; try ring.
-    apply gt_lt_symmetry.
+    rewrite Z.mul_div_eq; try ring.
+    apply Z.gt_lt_iff.
     apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg.
   Qed.
 
@@ -423,7 +423,7 @@ Section CarryProofs.
       rewrite <- Z.add_opp_l, <- Z.opp_sub_distr.
       unfold pow2_mod.
       rewrite Z.land_ones by apply log_cap_nonneg.
-      rewrite <- mul_div_eq by (apply gt_lt_symmetry; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg).
+      rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg).
       rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
       rewrite Zopp_mult_distr_r.
       rewrite Z.mul_comm.
@@ -570,7 +570,7 @@ Section CanonicalizationProofs.
 
   Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i.
   Proof.
-    unfold max_bound, log_cap; intros; apply Z_ones_pos_pos.
+    unfold max_bound, log_cap; intros; apply Z.ones_pos_pos.
     apply limb_widths_pos.
     rewrite nth_default_eq.
     apply nth_In.
@@ -580,7 +580,7 @@ Section CanonicalizationProofs.
 
   Lemma max_bound_nonneg : forall i, 0 <= max_bound i.
   Proof.
-    unfold max_bound; intros; auto using Z_ones_nonneg.
+    unfold max_bound; intros; auto using Z.ones_nonneg.
   Qed.
   Local Hint Resolve max_bound_nonneg.
 
@@ -939,7 +939,7 @@ Section CanonicalizationProofs.
     apply Z.add_le_mono.
     + apply carry_bounds_0_upper; auto; omega.
     + apply Z.mul_le_mono_pos_l; auto using c_pos.
-      apply Z_shiftr_ones; auto;
+      apply Z.shiftr_ones; auto;
         [ | pose proof (B_compat_log_cap (pred (length base))); omega ].
       split.
       - apply carry_bounds_lower; auto; omega.
@@ -978,7 +978,7 @@ Section CanonicalizationProofs.
     + rewrite <-max_bound_log_cap, <-Z.add_1_l.
       apply Z.add_le_mono.
       - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
-        apply Z_div_floor; auto.
+        apply Z.div_floor; auto.
         destruct i.
         * simpl.
           eapply Z.le_lt_trans; [ apply carry_full_bounds_0; auto | ].
@@ -1061,7 +1061,7 @@ Section CanonicalizationProofs.
     + rewrite <-max_bound_log_cap, <-Z.add_1_l.
       rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
       apply Z.add_le_mono.
-      - apply Z_div_floor; auto.
+      - apply Z.div_floor; auto.
         eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ].
         replace (Z.succ 1) with (2 ^ 1) by ring.
         rewrite <-max_bound_log_cap.
@@ -1267,7 +1267,7 @@ Section CanonicalizationProofs.
   Lemma max_ones_nonneg : 0 <= max_ones.
   Proof.
     unfold max_ones.
-    apply Z_ones_nonneg.
+    apply Z.ones_nonneg.
     pose proof limb_widths_nonneg.
     induction limb_widths.
     cbv; congruence.
@@ -1282,19 +1282,19 @@ Section CanonicalizationProofs.
     unfold max_ones.
     intros ? ? x_range.
     rewrite Z.land_comm.
-    rewrite Z.land_ones by apply Z_le_fold_right_max_initial.
+    rewrite Z.land_ones by apply Z.le_fold_right_max_initial.
     apply Z.mod_small.
     split; try omega.
     eapply Z.lt_le_trans; try eapply x_range.
     apply Z.pow_le_mono_r; try omega.
     rewrite log_cap_eq.
     destruct (lt_dec i (length limb_widths)).
-    + apply Z_le_fold_right_max.
+    + apply Z.le_fold_right_max.
       - apply limb_widths_nonneg.
       - rewrite nth_default_eq.
         auto using nth_In.
     + rewrite nth_default_out_of_bounds by omega.
-      apply Z_le_fold_right_max_initial.
+      apply Z.le_fold_right_max_initial.
   Qed.
 
   Lemma full_isFull'_true : forall j us, (length us = length base) ->
@@ -1802,7 +1802,7 @@ Section CanonicalizationProofs.
     + match goal with |- (?a ?= ?b) = (?c ?= ?d) =>
         rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end.
       apply CompOpp_inj; rewrite !CompOpp_involutive.
-      apply gt_lt_symmetry in Hgt.
+      apply Z.gt_lt_iff in Hgt.
       etransitivity; try apply Z_compare_decode_step_lt; auto; omega.
   Qed.
 
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 23393d7ef..1504ca0df 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -97,7 +97,7 @@ Section Pow2BaseProofs.
   Proof.
     intros.
     repeat rewrite nth_default_base by omega.
-    apply mod_same_pow.
+    apply Z.mod_same_pow.
     split; [apply sum_firstn_limb_widths_nonneg | ].
     destruct (NPeano.Nat.eq_dec i 0); subst.
       + case_eq limb_widths; intro; unfold sum_firstn; simpl; try omega; intros l' lw_eq.
@@ -199,7 +199,7 @@ Section BitwiseDecodeEncode.
     intros.
     simpl; f_equal.
     match goal with H : bounded _ _ |- _ => 
-      rewrite Z_lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end.
+      rewrite Z.lor_shiftl by (auto; unfold bounded in H; specialize (H i); assumption) end.
     rewrite Z.shiftl_mul_pow2 by auto.
     ring.
   Qed.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 2021e8514..a2f606f30 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -460,8 +460,8 @@ Section SquareRootsPrime5Mod8.
       apply Z2N.inj_iff; try zero_bounds.
       rewrite <- Z.mul_cancel_l with (p := 2) by omega.
       ring_simplify.
-      rewrite mul_div_eq by omega.
-      rewrite mul_div_eq by omega.
+      rewrite Z.mul_div_eq by omega.
+      rewrite Z.mul_div_eq by omega.
       rewrite (Zmod_div_mod 2 8 q) by
         (try omega; apply Zmod_divide; omega || auto).
       rewrite q_5mod8.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 50c1f3ea6..c07da850f 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -42,7 +42,7 @@ Section PseudoMersenneBaseParamProofs.
     rewrite (Z.mul_comm r).
     subst r.
     assert (i + j - length base < length base)%nat by omega.
-    rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.mul_pos_pos;
+    rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos;
       [ | subst b; unfold base; rewrite nth_default_base; try assumption ];
       zero_bounds; auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg).
     rewrite (Zminus_0_l_reverse (b i * b j)) at 1.
@@ -51,7 +51,7 @@ Section PseudoMersenneBaseParamProofs.
     unfold base; repeat rewrite nth_default_base by auto.
     do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
     symmetry.
-    apply mod_same_pow.
+    apply Z.mod_same_pow.
     split.
     + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg.
     + rewrite base_length, base_from_limb_widths_length in * by auto.
@@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs.
      destruct In_b_base as [i nth_err_b].
      apply nth_error_subst in nth_err_b; [ | auto ].
      rewrite nth_err_b.
-     apply gt_lt_symmetry.
+     apply Z.gt_lt_iff.
      apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg.
    Qed.
 
@@ -84,10 +84,10 @@ Section PseudoMersenneBaseParamProofs.
      unfold base in *.
      repeat rewrite nth_default_base by (omega || auto).
      rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))).
-     rewrite mul_div_eq by (apply gt_lt_symmetry; zero_bounds;
+     rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds;
        auto using sum_firstn_limb_widths_nonneg).
      rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
-     rewrite mod_same_pow; try ring.
+     rewrite Z.mod_same_pow; try ring.
      split; [ auto using sum_firstn_limb_widths_nonneg | ].
      apply limb_widths_good.
      rewrite <- base_length; assumption.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
new file mode 100644
index 000000000..7ec5d99ec
--- /dev/null
+++ b/src/Spec/WeierstrassCurve.v
@@ -0,0 +1,84 @@
+Require Crypto.WeierstrassCurve.Pre.
+
+Module E.
+  Section WeierstrassCurves.
+    (* Short Weierstrass curves with addition laws. References:
+     * <https://hyperelliptic.org/EFD/g1p/auto-shortw.html>
+     * <https://cr.yp.to/talks/2007.06.07/slides.pdf>
+     * See also:
+     * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79)
+     *)
+
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope.
+    Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "'∞'" := unit : type_scope.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3).
+    Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))).
+    Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))).
+    Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))).
+
+    Local Notation "( x , y )" := (inl (pair x y)).
+    Local Open Scope core_scope.
+
+    Context {a b: F}.
+
+    (** N.B. We may require more conditions to prove that points form
+        a group under addition (associativity, in particular.  If
+        that's the case, more fields will be added to this class. *)
+    Class weierstrass_params :=
+      {
+        char_gt_2 : 2 <> 0;
+        char_ne_3 : 3 <> 0;
+        nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0
+      }.
+    Context `{weierstrass_params}.
+
+    Definition point := { P | match P with
+                              | (x, y) => y^2 = x^3 + a*x + b
+                              | ∞ => True
+                              end }.
+    Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P.
+
+    (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *)
+    Local Obligation Tactic :=
+      try solve [ Program.Tactics.program_simpl
+                | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ].
+
+    Program Definition zero : point := ∞.
+
+    Program Definition add (P1 P2:point) : point
+      := exist
+           _
+           (match coordinates P1, coordinates P2 return _ with
+            | (x1, y1), (x2, y2) =>
+              if x1 =? x2 then
+                if y2 =? -y1 then          ∞
+                else                       ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1,
+                                             (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1)
+              else                         ((y2-y1)^2 / (x2-x1)^2 - x1 - x2,
+                                             (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1)
+            | ∞, ∞ =>                      ∞
+            | ∞, _ =>                      coordinates P2
+            | _, ∞ =>                      coordinates P1
+            end)
+           _.
+
+    Fixpoint mul (n:nat) (P : point) : point :=
+      match n with
+      | O => zero
+      | S n' => add P (mul n' P)
+      end.
+  End WeierstrassCurves.
+End E.
+
+Delimit Scope E_scope with E.
+Infix "+" := E.add : E_scope.
+Infix "*" := E.mul : E_scope.
diff --git a/src/Testbit.v b/src/Testbit.v
index 545c3cbce..f9de9092b 100644
--- a/src/Testbit.v
+++ b/src/Testbit.v
@@ -107,7 +107,7 @@ Proof.
     rewrite <- nth_default_eq in uniform.
     erewrite nth_error_value_eq_nth_default in uniform; eauto.
     subst.
-    destruct r; [ | apply pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega.
+    destruct r; [ | apply Z.pos_pow_nat_pos | pose proof (Zlt_neg_0 p) ] ; omega.
   + intros.
     rewrite nth_default_eq.
     rewrite uniform; auto.
@@ -151,7 +151,7 @@ Proof.
   induction us; boring.
   rewrite <- (IHus base) by (omega || eauto using no_overflow_tail).
   rewrite decode_cons by (eapply uniform_base_BaseVector; eauto;
-    rewrite gt_lt_symmetry; apply Z_pow_gt0; omega).
+    rewrite Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega).
   simpl.
   f_equal.
   + symmetry. eapply no_overflow_cons; eauto.
@@ -174,12 +174,12 @@ Proof.
     auto using Z.land_0_l.
   + destruct i; simpl.
     - rewrite nth_default_cons.
-      rewrite Z.shiftr_0_r, Z_land_add_land by omega.
+      rewrite Z.shiftr_0_r, Z.land_add_land by omega.
       symmetry; eapply no_overflow_cons; eauto.
     - rewrite nth_default_cons_S.
       erewrite IHus; eauto using no_overflow_tail.
       remember (i * limb_width)%nat as k.
-      rewrite Z_shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add;
+      rewrite Z.shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add;
         repeat f_equal; try omega.
       rewrite Z.land_ones by apply Nat2Z.is_nonneg.
       apply Z.mod_pos_bound. zero_bounds.
@@ -191,7 +191,7 @@ Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat ->
 Proof.
   unfold testbit; intros.
   erewrite unfold_bits_indexing; eauto.
-  rewrite <- Z_testbit_low by
+  rewrite <- Z.testbit_low by
     (split; try apply Nat2Z.inj_lt; pose proof (mod_bound_pos n limb_width); omega).
   rewrite Z.shiftr_spec by apply Nat2Z.is_nonneg.
   f_equal.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index bc2c8425b..0cdfd784f 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,4 +1,5 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
+Require Import Coq.micromega.Psatz.
 Import Nat.
 
 Local Open Scope nat_scope.
@@ -78,3 +79,10 @@ Proof.
     [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
     | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
 Qed.
+
+Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0.
+Proof.
+  intro; induction k; simpl; nia.
+Qed.
+
+Hint Resolve pow_nonzero : arith.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 10ce148b0..c16b87639 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -66,7 +66,7 @@ Qed.
 
 Lemma p_odd : Z.odd p = true.
 Proof.
-  pose proof (prime_odd_or_2 p prime_p).
+  pose proof (Z.prime_odd_or_2 p prime_p).
   destruct H; auto.
 Qed.
 
@@ -124,12 +124,12 @@ Proof.
   assert (b mod p <> 0) as b_nonzero. {
     intuition.
     rewrite <- Z.pow_2_r in a_square.
-    rewrite mod_exp_0 in a_square by prime_bound.
+    rewrite Z.mod_exp_0 in a_square by prime_bound.
     rewrite <- a_square in a_nonzero.
     auto.
   }
   pose proof (squared_fermat_little b b_nonzero).
-  rewrite mod_pow in * by prime_bound.
+  rewrite Z.mod_pow in * by prime_bound.
   rewrite <- a_square.
   rewrite Z.mod_mod; prime_bound.
 Qed.
@@ -172,10 +172,10 @@ Proof.
   intros.
   destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto.
   destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y.
-  rewrite mod_pow in pow_a_x by prime_bound.
+  rewrite Z.mod_pow in pow_a_x by prime_bound.
   replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega).
   rewrite <- pow_y_j in pow_a_x.
-  rewrite <- mod_pow in pow_a_x by prime_bound.
+  rewrite <- Z.mod_pow in pow_a_x by prime_bound.
   rewrite <- Z.pow_mul_r in pow_a_x by omega.
   assert (p - 1 | j * x) as divide_mul_j_x. {
     rewrite <- phi_is_order in y_order.
@@ -193,13 +193,13 @@ Proof.
   rewrite <- Z_div_plus by omega.
   rewrite Z.mul_comm.
   rewrite x_id_inv in divide_mul_j_x; auto.
-  apply (divide_mul_div _ j 2) in divide_mul_j_x;
+  apply (Z.divide_mul_div _ j 2) in divide_mul_j_x;
     try (apply prime_pred_divide2 || prime_bound); auto.
   rewrite <- Zdivide_Zdiv_eq by (auto || omega).
   rewrite Zplus_diag_eq_mult_2.
   replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega).
   rewrite Z_div_mult by omega; auto.
-  apply divide2_even_iff.
+  apply Z.divide2_even_iff.
   apply prime_pred_even.
 Qed.
 
@@ -281,7 +281,7 @@ Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2),
   (p / 2) * 2 + 1 = p.
 Proof.
   intros.
-  destruct (prime_odd_or_2 p prime_p); intuition.
+  destruct (Z.prime_odd_or_2 p prime_p); intuition.
   rewrite <- Zdiv2_div.
   pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega.
 Qed.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index abfc2499c..304ae3c20 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -229,6 +229,15 @@ Ltac destruct_sig_matcher HT :=
 Ltac destruct_sig := destruct_all_matches destruct_sig_matcher.
 Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher.
 
+(** try to specialize all non-dependent hypotheses using [tac] *)
+Ltac specialize_by' tac :=
+  idtac;
+  match goal with
+  | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by tac; specialize (H H'); clear H'
+  end.
+
+Ltac specialize_by tac := repeat specialize_by' tac.
+
 (** If [tac_in H] operates in [H] and leaves side-conditions before
     the original goal, then
     [side_conditions_before_to_side_conditions_after tac_in H] does
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 5ea174577..6a452169c 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,206 +1,250 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
 Require Import Coq.Lists.List.
 Import Nat.
 Local Open Scope Z.
 
-Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
-Proof.
-  intros; split; omega.
-Qed.
+Hint Extern 1 => lia : lia.
+Hint Extern 1 => lra : lra.
+Hint Extern 1 => nia : nia.
+Hint Extern 1 => omega : omega.
+Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l : zarith.
+Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith.
+
+(** Only hints that are always safe to apply (i.e., reversible), and
+    which can reasonably be said to "simplify" the goal, should go in
+    this database. *)
+Create HintDb zsimplify discriminated.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add using lia : zsimplify.
+
+(** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
+Create HintDb push_Zopp discriminated.
+Create HintDb pull_Zopp discriminated.
+Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp.
+Hint Rewrite Z.mul_opp_l : pull_Zopp.
+Hint Rewrite <- Z.opp_add_distr : pull_Zopp.
+Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp.
+Hint Rewrite <- Z.mul_opp_l : push_Zopp.
+Hint Rewrite Z.opp_add_distr : push_Zopp.
+
+Create HintDb push_Zmul discriminated.
+Create HintDb pull_Zmul discriminated.
+Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul.
+Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul.
+
+(** For the occasional lemma that can remove the use of [Z.div] *)
+Create HintDb zstrip_div.
+Hint Rewrite Z.div_small_iff using lia : zstrip_div.
+
+(** It's not clear that [mod] is much easier for [lia] than [Z.div],
+    so we separate out the transformations between [mod] and [div].
+    We'll put, e.g., [mul_div_eq] into it below. *)
+Create HintDb zstrip_div.
+
+Module Z.
+  Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
+  Proof. intros; omega. Qed.
+
+  Hint Resolve positive_is_nonzero : zarith.
+
+  Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
+    a / b > 0.
+  Proof.
+    intros; rewrite Z.gt_lt_iff.
+    apply Z.div_str_pos.
+    split; intuition.
+    apply Z.divide_pos_le; try (apply Zmod_divide); omega.
+  Qed.
 
-Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
-Proof.
-  intros; omega.
-Qed.
-Hint Resolve positive_is_nonzero.
+  Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
+  Proof. intros; subst; auto. Qed.
 
-Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
-  a / b > 0.
-Proof.
-  intros; rewrite gt_lt_symmetry.
-  apply Z.div_str_pos.
-  split; intuition.
-  apply Z.divide_pos_le; try (apply Zmod_divide); omega.
-Qed.
+  Hint Resolve elim_mod : zarith.
 
-Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
-Proof.
-  intros; subst; auto.
-Qed.
-Hint Resolve elim_mod.
+  Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
+  Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add_l using lia : zsimplify.
 
-Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b.
-Proof.
-  intros.
-  rewrite Zplus_mod.
-  rewrite Z.mod_mul; auto; simpl.
-  rewrite Zmod_mod; auto.
-Qed.
+  Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b.
+  Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a.
+  Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add' mod_add_l' using lia : zsimplify.
 
-Lemma pos_pow_nat_pos : forall x n,
-  Z.pos x ^ Z.of_nat n > 0.
-  do 2 (intros; induction n; subst; simpl in *; auto with zarith).
-  rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
-  apply Zmult_gt_0_compat; auto; reflexivity.
-Qed.
+  Lemma pos_pow_nat_pos : forall x n,
+    Z.pos x ^ Z.of_nat n > 0.
+  Proof.
+    do 2 (intros; induction n; subst; simpl in *; auto with zarith).
+    rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
+    apply Zmult_gt_0_compat; auto; reflexivity.
+  Qed.
 
-Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
-  intros. rewrite Z.mul_comm. apply Z.div_mul; auto.
-Qed.
+  Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
+  Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed.
+  Hint Rewrite div_mul' using lia : zsimplify.
 
-Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
-  intuition.
-Qed.
+  (** TODO: Should we get rid of this duplicate? *)
+  Notation gt0_neq0 := positive_is_nonzero (only parsing).
 
-Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
-  ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
-Proof.
-  intros; induction n; try reflexivity.
-  rewrite Nat2Z.inj_succ.
-  rewrite pow_succ_r by apply le_0_n.
-  rewrite Z.pow_succ_r by apply Zle_0_nat.
-  rewrite IHn.
-  rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
-Qed.
+  Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
+    ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
+  Proof.
+    intros; induction n; try reflexivity.
+    rewrite Nat2Z.inj_succ.
+    rewrite pow_succ_r by apply le_0_n.
+    rewrite Z.pow_succ_r by apply Zle_0_nat.
+    rewrite IHn.
+    rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
+  Qed.
 
-Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
-  a ^ x mod m = 0.
-Proof.
-  intros.
-  replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
-  induction (Z.to_nat x). {
-    simpl in *; omega.
-  } {
-    rewrite Nat2Z.inj_succ in *.
-    rewrite Z.pow_succ_r by omega.
-    rewrite Z.mul_mod by omega.
-    case_eq n; intros. {
-      subst. simpl.
-      rewrite Zmod_1_l by omega.
-      rewrite H1.
-      apply Zmod_0_l.
+  Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n.
+  Proof with auto using Zle_0_nat, Z.pow_nonneg.
+    intros; apply Z2Nat.inj...
+    rewrite <- pow_Z2N_Zpow, !Nat2Z.id...
+  Qed.
+
+  Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
+    a ^ x mod m = 0.
+  Proof.
+    intros.
+    replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
+    induction (Z.to_nat x). {
+      simpl in *; omega.
     } {
-      subst.
-      rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
-      rewrite H1.
-      auto.
+      rewrite Nat2Z.inj_succ in *.
+      rewrite Z.pow_succ_r by omega.
+      rewrite Z.mul_mod by omega.
+      case_eq n; intros. {
+        subst. simpl.
+        rewrite Zmod_1_l by omega.
+        rewrite H1.
+        apply Zmod_0_l.
+      } {
+        subst.
+        rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
+        rewrite H1.
+        auto.
+      }
     }
-  }
-Qed.
+  Qed.
 
-Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
-    a ^ b mod m = (a mod m) ^ b mod m.
-Proof.
-  intros; rewrite <- (Z2Nat.id b) by auto.
-  induction (Z.to_nat b); auto.
-  rewrite Nat2Z.inj_succ.
-  do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
-  rewrite Z.mul_mod by auto.
-  rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
-  rewrite <- IHn by auto.
-  rewrite Z.mod_mod by auto.
-  reflexivity.
-Qed.
+  Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
+      a ^ b mod m = (a mod m) ^ b mod m.
+  Proof.
+    intros; rewrite <- (Z2Nat.id b) by auto.
+    induction (Z.to_nat b); auto.
+    rewrite Nat2Z.inj_succ.
+    do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
+    rewrite Z.mul_mod by auto.
+    rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
+    rewrite <- IHn by auto.
+    rewrite Z.mod_mod by auto.
+    reflexivity.
+  Qed.
 
-Ltac Zdivide_exists_mul := let k := fresh "k" in
-match goal with
-| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
-| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
-end; (omega || auto).
+  Ltac divide_exists_mul := let k := fresh "k" in
+  match goal with
+  | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
+  | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
+  end; (omega || auto).
 
-Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
-  (a | b * (a / c)) -> (c | a) -> (c | b).
-Proof.
-  intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul.
-  rewrite divide_c_a in divide_a.
-  rewrite Z_div_mul' in divide_a by auto.
-  replace (b * k) with (k * b) in divide_a by ring.
-  replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
-  rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
-  eapply Zdivide_intro; eauto.
-Qed.
+  Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
+    (a | b * (a / c)) -> (c | a) -> (c | b).
+  Proof.
+    intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul.
+    rewrite divide_c_a in divide_a.
+    rewrite div_mul' in divide_a by auto.
+    replace (b * k) with (k * b) in divide_a by ring.
+    replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
+    rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
+    eapply Zdivide_intro; eauto.
+  Qed.
 
-Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
-Proof.
-  intro; split. {
-    intro divide2_n.
-    Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
-    rewrite divide2_n.
-    apply Z.even_mul.
-  } {
-    intro n_even.
-    pose proof (Zmod_even n).
-    rewrite n_even in H.
-    apply Zmod_divide; omega || auto.
-  }
-Qed.
+  Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
+  Proof.
+    intro; split. {
+      intro divide2_n.
+      divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
+      rewrite divide2_n.
+      apply Z.even_mul.
+    } {
+      intro n_even.
+      pose proof (Zmod_even n).
+      rewrite n_even in H.
+      apply Zmod_divide; omega || auto.
+    }
+  Qed.
 
-Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
-Proof.
-  intros.
-  apply Decidable.imp_not_l; try apply Z.eq_decidable.
-  intros p_neq2.
-  pose proof (Zmod_odd p) as mod_odd.
-  destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
-  rewrite p_not_odd in mod_odd.
-  apply Zmod_divides in mod_odd; try omega.
-  destruct mod_odd as [c c_id].
-  rewrite Z.mul_comm in c_id.
-  apply Zdivide_intro in c_id.
-  apply prime_divisors in c_id; auto.
-  destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
-  pose proof (prime_ge_2 p prime_p); omega.
-Qed.
+  Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
+  Proof.
+    intros.
+    apply Decidable.imp_not_l; try apply Z.eq_decidable.
+    intros p_neq2.
+    pose proof (Zmod_odd p) as mod_odd.
+    destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
+    rewrite p_not_odd in mod_odd.
+    apply Zmod_divides in mod_odd; try omega.
+    destruct mod_odd as [c c_id].
+    rewrite Z.mul_comm in c_id.
+    apply Zdivide_intro in c_id.
+    apply prime_divisors in c_id; auto.
+    destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
+    pose proof (prime_ge_2 p prime_p); omega.
+  Qed.
 
-Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z.
-Proof.
-  intros.
-  rewrite (Z_div_mod_eq a m) at 2 by auto.
-  ring.
-Qed.
+  Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m).
+  Proof.
+    intros.
+    rewrite (Z_div_mod_eq a m) at 2 by auto.
+    ring.
+  Qed.
 
-Ltac prime_bound := match goal with
-| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
-end.
+  Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z.
+  Proof.
+    intros.
+    rewrite (Z_div_mod_eq a m) at 2 by auto.
+    ring.
+  Qed.
 
-Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m.
-Proof.
-  intros; omega.
-Qed.
+  Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod.
+  Hint Rewrite <- mul_div_eq' using lia : zmod_to_div.
 
+  Ltac prime_bound := match goal with
+  | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
+  end.
 
-Lemma Z_testbit_low : forall n x i, (0 <= i < n) ->
-  Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i.
-Proof.
-  intros.
-  rewrite Z.land_ones by omega.
-  symmetry.
-  apply Z.mod_pow2_bits_low.
-  omega.
-Qed.
+  Lemma testbit_low : forall n x i, (0 <= i < n) ->
+    Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i.
+  Proof.
+    intros.
+    rewrite Z.land_ones by omega.
+    symmetry.
+    apply Z.mod_pow2_bits_low.
+    omega.
+  Qed.
 
-Lemma Z_testbit_add_shiftl_low : forall i a b n, (0 <= i < n) ->
-  Z.testbit (a + Z.shiftl b n) i = Z.testbit a i.
-Proof.
-  intros.
-  erewrite Z_testbit_low; eauto.
-  rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega.
-  rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).
-  apply Z.mod_pow2_bits_low.
-  omega.
-Qed.
 
+  Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) ->
+    Z.testbit (a + Z.shiftl b n) i = Z.testbit a i.
+  Proof.
+    intros.
+    erewrite Z.testbit_low; eauto.
+    rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega.
+    rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).
+    auto using Z.mod_pow2_bits_low.
+  Qed.
 
-Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
-Proof.
-  intros.
-  apply Z.div_small.
-  auto using Z.mod_pos_bound.
-Qed.
+  Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
+  Proof.
+    intros.
+    apply Z.div_small.
+    auto using Z.mod_pos_bound.
+  Qed.
+  Hint Rewrite mod_div_eq0 using lia : zsimplify.
 
-Lemma Z_shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n ->
+Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n ->
   Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n).
 Proof.
   intros.
@@ -212,7 +256,7 @@ Proof.
   f_equal; ring.
 Qed.
 
-Lemma Z_shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n ->
+Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n ->
   Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n).
 Proof.
   intros.
@@ -223,7 +267,7 @@ Proof.
   repeat f_equal; ring.
 Qed.
 
-Lemma Z_testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) ->
+Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) ->
   0 <= a < 2 ^ n ->
   Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n).
 Proof.
@@ -233,7 +277,7 @@ Proof.
      replace a with 0 by omega; f_equal; ring | ]); try omega.
   rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption.
   replace (Z.succ x - n) with (x - (n - 1)) by ring.
-  rewrite Z_shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega.
+  rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega.
   rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ].
   rewrite Z.shiftr_div_pow2 by omega.
   split; apply Z.div_pos || apply Z.div_lt_upper_bound;
@@ -242,89 +286,81 @@ Proof.
   replace (1 + (n - 1)) with n by ring; omega.
 Qed.
 
-Lemma Z_land_add_land : forall n m a b, (m <= n)%nat ->
-  Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).
-Proof.
-  intros.
-  rewrite !Z.land_ones by apply Nat2Z.is_nonneg.
-  rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
-  replace (b * 2 ^ Z.of_nat n) with
-    ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by
-    (rewrite (le_plus_minus m n) at 2; try assumption;
-     rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
-  rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega).
-  symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega).
-  rewrite (le_plus_minus m n) by assumption.
-  rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
-  apply Z.divide_factor_l.
-Qed.
-
-Lemma Z_pow_gt0 : forall a, 0 < a -> forall b, 0 <= b -> 0 < a ^ b.
-Proof.
-  intros until 1.
-  apply natlike_ind; try (simpl; omega).
-  intros.
-  rewrite Z.pow_succ_r by assumption.
-  apply Z.mul_pos_pos; assumption.
-Qed.
+  Lemma land_add_land : forall n m a b, (m <= n)%nat ->
+    Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).
+  Proof.
+    intros.
+    rewrite !Z.land_ones by apply Nat2Z.is_nonneg.
+    rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
+    replace (b * 2 ^ Z.of_nat n) with
+      ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by
+      (rewrite (le_plus_minus m n) at 2; try assumption;
+       rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
+    rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega).
+    symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega).
+    rewrite (le_plus_minus m n) by assumption.
+    rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
+    apply Z.divide_factor_l.
+  Qed.
 
-Lemma div_pow2succ : forall n x, (0 <= x) ->
-  n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
-Proof.
-  intros.
-  rewrite Z.pow_succ_r, Z.mul_comm by auto.
-  rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
-  rewrite Zdiv2_div.
-  reflexivity.
-Qed.
+  Lemma div_pow2succ : forall n x, (0 <= x) ->
+    n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
+  Proof.
+    intros.
+    rewrite Z.pow_succ_r, Z.mul_comm by auto.
+    rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
+    rewrite Zdiv2_div.
+    reflexivity.
+  Qed.
 
-Lemma shiftr_succ : forall n x,
-  Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
-Proof.
-  intros.
-  rewrite Z.shiftr_shiftr by omega.
-  reflexivity.
-Qed.
+  Lemma shiftr_succ : forall n x,
+    Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
+  Proof.
+    intros.
+    rewrite Z.shiftr_shiftr by omega.
+    reflexivity.
+  Qed.
 
 
-Definition Z_shiftl_by n a := Z.shiftl a n.
+  Definition shiftl_by n a := Z.shiftl a n.
 
-Lemma Z_shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z_shiftl_by n a.
-Proof.
-  intros.
-  unfold Z_shiftl_by.
-  rewrite Z.shiftl_mul_pow2 by assumption.
-  apply Z.mul_comm.
-Qed.
+  Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a.
+  Proof.
+    intros.
+    unfold Z.shiftl_by.
+    rewrite Z.shiftl_mul_pow2 by assumption.
+    apply Z.mul_comm.
+  Qed.
 
-Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z_shiftl_by n) l.
-Proof.
-  intros; induction l; auto using Z_shiftl_by_mul_pow2.
-  simpl.
-  rewrite IHl.
-  f_equal.
-  apply Z_shiftl_by_mul_pow2.
-  assumption.
-Qed.
+  Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l.
+  Proof.
+    intros; induction l; auto using Z.shiftl_by_mul_pow2.
+    simpl.
+    rewrite IHl.
+    f_equal.
+    apply Z.shiftl_by_mul_pow2.
+    assumption.
+  Qed.
 
-Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
-  Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
-Proof.
-  intros.
-  rewrite Zmod_eq_full by assumption.
-  rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
-  case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
-Qed.
+  Lemma odd_mod : forall a b, (b <> 0)%Z ->
+    Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+  Proof.
+    intros.
+    rewrite Zmod_eq_full by assumption.
+    rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+    case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+  Qed.
 
-Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
-Proof.
-  intros.
-  replace b with (b - c + c) by ring.
-  rewrite Z.pow_add_r by omega.
-  apply Z_mod_mult.
-Qed.
+  Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
+  Proof.
+    intros.
+    replace b with (b - c + c) by ring.
+    rewrite Z.pow_add_r by omega.
+    apply Z_mod_mult.
+  Qed.
+  Hint Rewrite mod_same_pow using lia : zsimplify.
 
-  Lemma Z_ones_succ : forall x, (0 <= x) ->
+  Lemma ones_succ : forall x, (0 <= x) ->
     Z.ones (Z.succ x) = 2 ^ x + Z.ones x.
   Proof.
     unfold Z.ones; intros.
@@ -335,14 +371,14 @@ Qed.
     rewrite Z.pow_succ_r; omega.
   Qed.
 
-  Lemma Z_div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c.
+  Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c.
   Proof.
     intros.
     apply Z.lt_succ_r.
     apply Z.div_lt_upper_bound; try omega.
   Qed.
 
-  Lemma Z_shiftr_1_r_le : forall a b, a <= b ->
+  Lemma shiftr_1_r_le : forall a b, a <= b ->
     Z.shiftr a 1 <= Z.shiftr b 1.
   Proof.
     intros.
@@ -350,7 +386,7 @@ Qed.
     apply Z.div_le_mono; omega.
   Qed.
 
-  Lemma Z_ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
+  Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
   Proof.
     induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.
     intros.
@@ -364,7 +400,7 @@ Qed.
     f_equal. omega.
   Qed.
 
-  Lemma Z_shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
+  Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
     Z.shiftr a i <= Z.ones (n - i) \/ n <= i.
   Proof.
     intros until 1.
@@ -378,17 +414,17 @@ Qed.
       left.
       rewrite shiftr_succ.
       replace (n - Z.succ x) with (Z.pred (n - x)) by omega.
-      rewrite Z_ones_pred by omega.
-      apply Z_shiftr_1_r_le.
+      rewrite Z.ones_pred by omega.
+      apply Z.shiftr_1_r_le.
       assumption.
   Qed.
 
-  Lemma Z_shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) ->
+  Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) ->
     Z.shiftr a i <= Z.ones (n - i) .
   Proof.
     intros a n i G G0 G1.
     destruct (Z_le_lt_eq_dec i n G1).
-    + destruct (Z_shiftr_ones' a n G i G0); omega.
+    + destruct (Z.shiftr_ones' a n G i G0); omega.
     + subst; rewrite Z.sub_diag.
       destruct (Z_eq_dec a 0).
       - subst; rewrite Z.shiftr_0_l; reflexivity.
@@ -396,7 +432,7 @@ Qed.
         apply Z.log2_lt_pow2; omega.
   Qed.
 
-  Lemma Z_shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1.
+  Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1.
   Proof.
     intros a ? ? [a_nonneg a_upper_bound].
     apply Z_le_lt_eq_dec in a_upper_bound.
@@ -412,107 +448,17 @@ Qed.
       omega.
   Qed.
 
-(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
-Ltac zero_bounds' :=
-  repeat match goal with
-  | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
-  | [ |- 0 <= _ - _] => apply Z.le_0_sub
-  | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
-  | [ |- 0 <= _ / _] => apply Z.div_pos
-  | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
-  | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
-  | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
-                       try solve [apply Z.add_nonneg_pos; zero_bounds']
-  | [ |- 0 < _ - _] => apply Z.lt_0_sub
-  | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
-  | [ |- 0 < _ / _] => apply Z.div_str_pos
-  | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
-  end; try omega; try prime_bound; auto.
-
-Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
-
-Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
-Proof.
-  apply natlike_ind.
-  + unfold Z.ones. simpl; omega.
-  + intros.
-    rewrite Z_ones_succ by assumption.
-    zero_bounds.
-Qed.
-
-Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
-Proof.
-  intros.
-  unfold Z.ones.
-  rewrite Z.shiftl_1_l.
-  apply Z.lt_succ_lt_pred.
-  apply Z.pow_gt_1; omega.
-Qed.
-
-Lemma N_le_1_l : forall p, (1 <= N.pos p)%N.
-Proof.
-  destruct p; cbv; congruence.
-Qed.
-
-Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
-Proof.
-  induction a; destruct b; intros; try solve [cbv; congruence];
-    simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
-    try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
-    rewrite land_eq in *; unfold N.le, N.compare in *;
-    rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
-    try assumption.
-  destruct (p ?=a)%positive; cbv; congruence.
-Qed.
-
-Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
-  Z.land a b <= a.
-Proof.
-  intros.
-  destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
-  cbv [Z.land].
-  rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
-  auto using Pos_land_upper_bound_l.
-Qed.
-
-Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) ->
-  Z.land a b <= b.
-Proof.
-  intros.
-  rewrite Z.land_comm.
-  auto using Z_land_upper_bound_l.
-Qed.
-
-Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
-  In x l -> x <= fold_right Z.max low l.
-Proof.
-  induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
-  simpl.
-  destruct (in_inv In_list); subst.
-  + apply Z.le_max_l.
-  + etransitivity.
-    - apply IHl; auto; intuition.
-    - apply Z.le_max_r.
-Qed.
-
-Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
-Proof.
-  induction l; intros; try reflexivity.
-  etransitivity; [ apply IHl | apply Z.le_max_r ].
-Qed.
-
-  (* TODO : move to ZUtil *)
-  Lemma Z_lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n ->
+  Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n ->
     Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n).
   Proof.
     intros.
     apply Z.bits_inj'; intros t ?.
     rewrite Z.lor_spec, Z.shiftl_spec by assumption.
     destruct (Z_lt_dec t n).
-    + rewrite Z_testbit_add_shiftl_low by omega.
+    + rewrite testbit_add_shiftl_low by omega.
       rewrite Z.testbit_neg_r with (n := t - n) by omega.
       apply Bool.orb_false_r.
-    + rewrite Z_testbit_add_shiftl_high by omega.
+    + rewrite testbit_add_shiftl_high by omega.
       replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ].
       symmetry.
       apply Z.testbit_false; try omega.
@@ -520,3 +466,446 @@ Qed.
       split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega.
       apply Z.pow_le_mono_r; omega.
   Qed.
+
+  (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
+  Ltac zero_bounds' :=
+    repeat match goal with
+    | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
+    | [ |- 0 <= _ - _] => apply Z.le_0_sub
+    | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
+    | [ |- 0 <= _ / _] => apply Z.div_pos
+    | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
+    | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
+    | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
+                         try solve [apply Z.add_nonneg_pos; zero_bounds']
+    | [ |- 0 < _ - _] => apply Z.lt_0_sub
+    | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
+    | [ |- 0 < _ / _] => apply Z.div_str_pos
+    | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
+    end; try omega; try prime_bound; auto.
+
+  Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
+
+  Hint Extern 1 => progress zero_bounds : zero_bounds.
+
+  Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
+  Proof.
+    apply natlike_ind.
+    + unfold Z.ones. simpl; omega.
+    + intros.
+      rewrite Z.ones_succ by assumption.
+      zero_bounds.
+  Qed.
+
+  Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
+  Proof.
+    intros.
+    unfold Z.ones.
+    rewrite Z.shiftl_1_l.
+    apply Z.lt_succ_lt_pred.
+    apply Z.pow_gt_1; omega.
+  Qed.
+
+  Lemma N_le_1_l : forall p, (1 <= N.pos p)%N.
+  Proof.
+    destruct p; cbv; congruence.
+  Qed.
+
+  Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
+  Proof.
+    induction a; destruct b; intros; try solve [cbv; congruence];
+      simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
+      try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
+      rewrite land_eq in *; unfold N.le, N.compare in *;
+      rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
+      try assumption.
+    destruct (p ?=a)%positive; cbv; congruence.
+  Qed.
+
+  Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
+    Z.land a b <= a.
+  Proof.
+    intros.
+    destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
+    cbv [Z.land].
+    rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
+    auto using Pos_land_upper_bound_l.
+  Qed.
+
+  Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) ->
+    Z.land a b <= b.
+  Proof.
+    intros.
+    rewrite Z.land_comm.
+    auto using Z.land_upper_bound_l.
+  Qed.
+
+  Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
+    In x l -> x <= fold_right Z.max low l.
+  Proof.
+    induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
+    simpl.
+    destruct (in_inv In_list); subst.
+    + apply Z.le_max_l.
+    + etransitivity.
+      - apply IHl; auto; intuition.
+      - apply Z.le_max_r.
+  Qed.
+
+  Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
+  Proof.
+    induction l; intros; try reflexivity.
+    etransitivity; [ apply IHl | apply Z.le_max_r ].
+  Qed.
+
+  Ltac ltb_to_lt :=
+    repeat match goal with
+           | [ H : (?x <? ?y) = ?b |- _ ]
+             => let H' := fresh in
+                rename H into H';
+                pose proof (Zlt_cases x y) as H;
+                rewrite H' in H;
+                clear H'
+           end.
+
+  Ltac compare_to_sgn :=
+    repeat match goal with
+           | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H
+           | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff
+           end.
+
+  Local Ltac replace_to_const c :=
+    repeat match goal with
+           | [ H : ?x = ?x |- _ ] => clear H
+           | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H'
+           | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H'
+           | [ H : ?x = c |- context[?x] ] => rewrite H
+           | [ H : c = ?x |- context[?x] ] => rewrite <- H
+           end.
+
+  Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)).
+  Proof.
+    Z.compare_to_sgn; rewrite Z.sgn_opp; simpl.
+    pose proof (Zdiv_sgn n m) as H.
+    pose proof (Z.sgn_spec (n / m)) as H'.
+    repeat first [ progress intuition
+                 | progress simpl in *
+                 | congruence
+                 | lia
+                 | progress replace_to_const (-1)
+                 | progress replace_to_const 0
+                 | progress replace_to_const 1
+                 | match goal with
+                   | [ x : Z |- _ ] => destruct x
+                   end ].
+  Qed.
+
+  Lemma two_times_x_minus_x x : 2 * x - x = x.
+  Proof. lia. Qed.
+
+  Lemma mul_div_le x y z
+        (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z)
+        (Hyz : y <= z)
+    : x * y / z <= x.
+  Proof.
+    transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ].
+    apply Z_div_le; nia.
+  Qed.
+
+  Lemma div_mul_diff a b c
+        (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
+    : c * a / b - c * (a / b) <= c.
+  Proof.
+    pose proof (Z.mod_pos_bound a b).
+    etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ].
+    rewrite (Z_div_mod_eq a b) at 1 by lia.
+    rewrite Z.mul_add_distr_l.
+    replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia.
+    rewrite Z.div_add_l by lia.
+    lia.
+  Qed.
+
+  Lemma div_mul_le_le a b c
+    :  0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c.
+  Proof.
+    pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia.
+  Qed.
+
+  Lemma div_mul_le_le_offset a b c
+    : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b).
+  Proof.
+    pose proof (Z.div_mul_le_le a b c); lia.
+  Qed.
+
+  Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith.
+
+  (** * [Z.simplify_fractions_le] *)
+  (** The culmination of this series of tactics,
+      [Z.simplify_fractions_le], will use the fact that [a * (b / c) <=
+      (a * b) / c], and do some reasoning modulo associativity and
+      commutativity in [Z] to perform such a reduction.  It may leave
+      over goals if it cannot prove that some denominators are non-zero.
+      If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the
+      LHS of the goal, this tactic should not turn a solvable goal into
+      an unsolvable one.
+
+      After running, the tactic does some basic rewriting to simplify
+      fractions, e.g., that [a * b / b = a]. *)
+  Ltac split_sums_step :=
+    match goal with
+    | [ |- _ + _ <= _ ]
+      => etransitivity; [ eapply Z.add_le_mono | ]
+    | [ |- _ - _ <= _ ]
+      => etransitivity; [ eapply Z.sub_le_mono | ]
+    end.
+  Ltac split_sums :=
+    try (split_sums_step; [ split_sums.. | ]).
+  Ltac pre_reorder_fractions_step :=
+    match goal with
+    | [ |- context[?x / ?y * ?z] ]
+      => rewrite (Z.mul_comm (x / y) z)
+    | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
+           match LHS with
+           | context G[?x * (?y / ?z)]
+             => let G' := context G[(x * y) / z] in
+                transitivity G'
+           end
+    end.
+  Ltac pre_reorder_fractions :=
+    try first [ split_sums_step; [ pre_reorder_fractions.. | ]
+              | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ].
+  Ltac split_comparison :=
+    match goal with
+    | [ |- ?x <= ?x ] => reflexivity
+    | [ H : _ >= _ |- _ ]
+      => apply Z.ge_le_iff in H
+    | [ |- ?x * ?y <= ?z * ?w ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
+         end;
+         [ ..
+         | lazymatch goal with
+           | [ H : 0 <= y |- _ ] => idtac
+           | [ H : y < 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec y 0)
+           end;
+           [ ..
+           | apply Zmult_le_compat; [ | | assumption | assumption ] ] ]
+    | [ |- ?x / ?y <= ?z / ?y ]
+      => lazymatch goal with
+         | [ H : 0 < y |- _ ] => idtac
+         | [ H : y <= 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec 0 y)
+         end;
+         [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ]
+         | .. ]
+    | [ |- ?x / ?y <= ?x / ?z ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
+         end;
+         [ ..
+         | lazymatch goal with
+           | [ H : 0 < z |- _ ] => idtac
+           | [ H : z <= 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec 0 z)
+           end;
+           [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ]
+           | .. ] ]
+    | [ |- _ + _ <= _ + _ ]
+      => apply Z.add_le_mono
+    | [ |- _ - _ <= _ - _ ]
+      => apply Z.sub_le_mono
+    | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ]
+      => apply Z.div_mul_le
+    end.
+  Ltac split_comparison_fin_step :=
+    match goal with
+    | _ => assumption
+    | _ => lia
+    | _ => progress subst
+    | [ H : ?n * ?m < 0 |- _ ]
+      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
+    | [ H : ?n / ?m < 0 |- _ ]
+      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
+    | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
+      => assert (0 <= x^y) by zero_bounds; lia
+    | [ H : (?x^?y) < 0 |- _ ]
+      => assert (0 <= x^y) by zero_bounds; lia
+    | [ H : (?x^?y) <= 0 |- _ ]
+      => let H' := fresh in
+         assert (H' : 0 <= x^y) by zero_bounds;
+         assert (x^y = 0) by lia;
+         clear H H'
+    | [ H : _^_ = 0 |- _ ]
+      => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
+    | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
+      => assert (x = 0) by lia; clear H H'
+    | [ |- ?x <= ?y ] => is_evar x; reflexivity
+    | [ |- ?x <= ?y ] => is_evar y; reflexivity
+    end.
+  Ltac split_comparison_fin := repeat split_comparison_fin_step.
+  Ltac simplify_fractions_step :=
+    match goal with
+    | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds)
+    | [ |- context[?x * ?y / ?x] ]
+      => rewrite (Z.mul_comm x y)
+    | [ |- ?x <= ?x ] => reflexivity
+    end.
+  Ltac simplify_fractions := repeat simplify_fractions_step.
+  Ltac simplify_fractions_le :=
+    pre_reorder_fractions;
+    [ repeat split_comparison; split_comparison_fin; zero_bounds..
+    | simplify_fractions ].
+
+  Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a.
+  Proof.
+    intros; transitivity 0; auto with zarith.
+  Qed.
+
+  Hint Resolve log2_nonneg' : zarith.
+
+  (** We create separate databases for two directions of transformations
+      involving [Z.log2]; combining them leads to loops. *)
+  (* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *)
+  Create HintDb hyp_log2.
+
+  (* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *)
+  Create HintDb concl_log2.
+
+  Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
+  Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
+
+  Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z.
+  Proof.
+    destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia.
+  Qed.
+
+  Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia.
+    reflexivity.
+  Qed.
+
+  Hint Rewrite div_x_y_x using lia : zsimplify.
+
+  Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0.
+  Proof.
+    split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption.
+  Qed.
+
+  Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+  Proof. lia. Qed.
+
+  Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify.
+  Hint Rewrite opp_eq_0_iff : zsimplify.
+
+  Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X.
+  Proof. lia. Qed.
+
+  Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity.
+  Qed.
+
+  Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia.
+  Qed.
+
+  Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp.
+  Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp.
+
+  Lemma div_opp a : a <> 0 -> -a / a = -1.
+  Proof.
+    intros; autorewrite with pull_Zopp zsimplify; lia.
+  Qed.
+
+  Hint Rewrite Z.div_opp using lia : zsimplify.
+
+  Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0.
+  Proof. auto with zarith lia. Qed.
+
+  Hint Rewrite div_sub_1_0 using lia : zsimplify.
+
+  Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0.
+  Proof.
+    intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1).
+    assert (Hn : -X <= a - b) by lia.
+    assert (Hp : a - b <= X - 1) by lia.
+    split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ];
+      instantiate; autorewrite with zsimplify; try reflexivity.
+  Qed.
+
+  Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1))
+       (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
+
+  Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0.
+  Proof.
+    intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1).
+    destruct (a <? b) eqn:?; Z.ltb_to_lt.
+    { cut ((a - b) / X <> 0); [ lia | ].
+      autorewrite with zstrip_div; auto with zarith lia. }
+    { autorewrite with zstrip_div; auto with zarith lia. }
+  Qed.
+
+  Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0.
+  Proof.
+    rewrite !(Z.add_comm (-_)), !Z.add_opp_r.
+    apply Z.sub_pos_bound_div_eq.
+  Qed.
+
+  Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using lia : zstrip_div.
+
+  Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b.
+  Proof. intros; symmetry; apply Z.div_small; assumption. Qed.
+
+  Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b.
+  Proof. intros; symmetry; apply Z.mod_small; assumption. Qed.
+
+  Hint Resolve div_small_sym mod_small_sym : zarith.
+
+  Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b.
+  Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed.
+
+  Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b.
+  Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed.
+
+  Hint Rewrite div_add_l' div_add' using lia : zsimplify.
+
+  Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed.
+
+  Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed.
+
+  Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed.
+
+  Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed.
+
+  Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify.
+
+  Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+
+  Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+
+  Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify.
+End Z.
+
+Module Export BoundsTactics.
+  Ltac prime_bound := Z.prime_bound.
+  Ltac zero_bounds := Z.zero_bounds.
+End BoundsTactics.
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
new file mode 100644
index 000000000..060d2f479
--- /dev/null
+++ b/src/WeierstrassCurve/Pre.v
@@ -0,0 +1,57 @@
+Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
+Require Import Crypto.Algebra Crypto.Tactics.Nsatz.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope core_scope.
+
+Generalizable All Variables.
+Section Pre.
+  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Notation "0" := zero.  Local Notation "1" := one.
+  Local Infix "+" := add. Local Infix "*" := mul.
+  Local Infix "-" := sub. Local Infix "/" := div.
+  Local Notation "- x" := (opp x).
+  Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
+  Local Notation "'∞'" := unit : type_scope.
+  Local Notation "'∞'" := (inr tt) : core_scope.
+  Local Notation "2" := (1+1). Local Notation "3" := (1+2).
+  Local Notation "( x , y )" := (inl (pair x y)).
+
+  Add Field WeierstrassCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
+  Add Ring WeierstrassCurveRing : (Ring.ring_theory_for_stdlib_tactic (T:=F)).
+
+  Context {a:F}.
+  Context {b:F}.
+
+  (* the canonical definitions are in Spec *)
+  Definition onCurve (P:F*F + ∞) := match P with
+                                    | (x, y) => y^2 = x^3 + a*x + b
+                                    | ∞ => True
+                                    end.
+  Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ :=
+    match P1', P2' with
+    | (x1, y1), (x2, y2)
+      => if x1 =? x2 then
+           if y2 =? -y1 then
+             ∞
+           else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1,
+                   (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1)
+         else
+           ((y2-y1)^2 / (x2-x1)^2 - x1 - x2,
+            (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1)
+    | ∞, ∞ => ∞
+    | ∞, _ => P2'
+    | _, ∞ => P1'
+    end.
+
+  Lemma unifiedAdd'_onCurve : forall P1 P2,
+    onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
+  Proof.
+    unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2;
+      break_match; trivial; setoid_subst_rel eq; only_two_square_roots;
+        field_algebra; nsatz_contradict.
+  Qed.
+End Pre.