Merge

16 files changed, 152 insertions, 142 deletions

diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index e6ad55f18..c07aad759 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -1,7 +1,8 @@
 Require Import Coq.Lists.List.
-Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Import Nat.
 
 Local Open Scope Z.
 
@@ -39,7 +40,7 @@ Section BaseSystem.
   Proof.
     unfold decode'; intros; f_equal; apply combine_truncate_l.
   Qed.
-  
+
   Fixpoint add (us vs:digits) : digits :=
     match us,vs with
       | u::us', v::vs' => u+v :: add us' vs'
@@ -58,26 +59,26 @@ Section BaseSystem.
       | nil, v::vs' => (0-v)::sub nil vs'
     end.
 
-  Definition crosscoef i j : Z := 
+  Definition crosscoef i j : Z :=
     let b := nth_default 0 base in
     (b(i) * b(j)) / b(i+j)%nat.
   Hint Unfold crosscoef.
 
   Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end.
-  
+
   (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *)
-  Fixpoint mul_bi' (i:nat) (vsr:digits) := 
+  Fixpoint mul_bi' (i:nat) (vsr:digits) :=
     match vsr with
     | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr'
     | nil => nil
     end.
   Definition mul_bi (i:nat) (vs:digits) : digits :=
     zeros i ++ rev (mul_bi' i (rev vs)).
-  
+
   (* mul' is multiplication with the FIRST ARGUMENT REVERSED *)
   Fixpoint mul' (usr vs:digits) : digits :=
     match usr with
-      | u::usr' => 
+      | u::usr' =>
         mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs
       | _ => nil
     end.
@@ -87,7 +88,7 @@ End BaseSystem.
 
 (* Example : polynomial base system *)
 Section PolynomialBaseCoefs.
-  Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true).
+  Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : ltb 0 baseLength = true).
   (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *)
   Definition bi i := (Zpos b1)^(Z.of_nat i).
   Definition poly_base := map bi (seq 0 baseLength).
@@ -96,7 +97,7 @@ Section PolynomialBaseCoefs.
     unfold poly_base, bi, nth_default.
     case_eq baseLength; intros. {
       assert ((0 < baseLength)%nat) by
-        (rewrite <-NPeano.ltb_lt; apply baseLengthNonzero).
+        (rewrite <-ltb_lt; apply baseLengthNonzero).
       subst; omega.
     }
     auto.
@@ -119,7 +120,7 @@ Section PolynomialBaseCoefs.
   Qed.
 
   Lemma poly_base_succ :
-    forall i, ((S i) < length poly_base)%nat -> 
+    forall i, ((S i) < length poly_base)%nat ->
     let b := nth_default 0 poly_base in
     let r := (b (S i) / b i) in
     b (S i) = r * b i.
@@ -127,7 +128,7 @@ Section PolynomialBaseCoefs.
     intros; subst b; subst r.
     repeat rewrite poly_base_defn in * by omega.
     unfold bi.
-    replace (Z.pos b1 ^ Z.of_nat (S i)) 
+    replace (Z.pos b1 ^ Z.of_nat (S i))
       with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by
       (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition).
     replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i)
@@ -166,7 +167,7 @@ Import ListNotations.
 
 Section BaseSystemExample.
   Definition baseLength := 32%nat.
-  Lemma baseLengthNonzero : NPeano.ltb 0 baseLength = true.
+  Lemma baseLengthNonzero : ltb 0 baseLength = true.
     compute; reflexivity.
   Qed.
   Definition base2 := poly_base 2 baseLength.
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index a2ebb7b41..dfb9f5bdf 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -18,7 +18,7 @@ Section BaseSystemProofs.
   Qed.
 
   Lemma decode'_splice : forall xs ys bs,
-    decode' bs (xs ++ ys) = 
+    decode' bs (xs ++ ys) =
     decode' (firstn (length xs) bs) xs + decode'  (skipn (length xs) bs) ys.
   Proof.
     unfold decode'.
@@ -83,7 +83,7 @@ Section BaseSystemProofs.
     unfold decode, encode; destruct z; boring.
   Qed.
 
-  Lemma mul_each_base : forall us bs c, 
+  Lemma mul_each_base : forall us bs c,
       decode' bs (mul_each c us) = decode' (mul_each c bs) us.
   Proof.
     induction us; destruct bs; boring; ring.
@@ -99,8 +99,8 @@ Section BaseSystemProofs.
     induction us; destruct low; boring.
   Qed.
 
-  Lemma base_mul_app : forall low c us, 
-      decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + 
+  Lemma base_mul_app : forall low c us,
+      decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) +
       c * decode' low (skipn (length low) us).
   Proof.
     intros.
@@ -118,7 +118,7 @@ Section BaseSystemProofs.
   Qed.
   Hint Rewrite length_zeros.
 
-  Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m).
+  Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m)%nat.
   Proof.
     induction n; boring.
   Qed.
@@ -237,7 +237,7 @@ Section BaseSystemProofs.
 
   Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n.
     induction n; auto.
-    simpl; f_equal; auto. 
+    simpl; f_equal; auto.
   Qed.
 
   Lemma mul_bi'_n_nil : forall n, mul_bi' base n nil = nil.
@@ -255,13 +255,13 @@ Section BaseSystemProofs.
     induction us; auto.
   Qed.
   Hint Rewrite add_nil_r.
-  
+
   Lemma add_first_terms : forall us vs a b,
     (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs).
     auto.
   Qed.
   Hint Rewrite add_first_terms.
- 
+
   Lemma mul_bi'_cons : forall n x us,
     mul_bi' base n (x :: us) = x * crosscoef base n (length us) :: mul_bi' base n us.
   Proof.
@@ -278,7 +278,7 @@ Section BaseSystemProofs.
   Hint Rewrite app_nil_l.
   Hint Rewrite app_nil_r.
 
-  Lemma add_snoc_same_length : forall l us vs a b, 
+  Lemma add_snoc_same_length : forall l us vs a b,
     (length us = l) -> (length vs = l) ->
     (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil.
   Proof.
@@ -288,7 +288,7 @@ Section BaseSystemProofs.
   Lemma mul_bi'_add : forall us n vs l
     (Hlus: length us = l)
     (Hlvs: length vs = l),
-    mul_bi' base n (rev (us .+ vs)) = 
+    mul_bi' base n (rev (us .+ vs)) =
     mul_bi' base n (rev us) .+ mul_bi' base n (rev vs).
   Proof.
     (* TODO(adamc): please help prettify this *)
@@ -322,7 +322,7 @@ Section BaseSystemProofs.
   Proof.
     induction n; boring.
   Qed.
-  
+
   Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) ->
     (rev us) .+ (rev vs) = rev (us .+ vs).
   Proof.
@@ -364,7 +364,7 @@ Section BaseSystemProofs.
   Hint Rewrite minus_diag.
 
   Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat ->
-    us .+ vs = us .+ (vs ++ (zeros (length us - length vs))).
+    us .+ vs = us .+ (vs ++ (zeros (length us - length vs)%nat)).
   Proof.
     induction us, vs; boring; f_equal; boring.
   Qed.
@@ -462,7 +462,7 @@ Section BaseSystemProofs.
   (* mul' is multiplication with the FIRST ARGUMENT REVERSED *)
   Fixpoint mul' (usr vs:digits) : digits :=
     match usr with
-      | u::usr' => 
+      | u::usr' =>
         mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs
       | _ => nil
     end.
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..f10e587d6 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,9 +1,11 @@
 Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Coq.omega.Omega.
 
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope Z_scope.
 Local Open Scope F_scope.
-  
+
 Section Pre.
   Context {q : BinInt.Z}.
   Context {a : F q}.
@@ -20,8 +22,8 @@ Section Pre.
      postprocess [Fpostprocess],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   (* the canonical definitions are in Spec *)
   Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
   Local Notation unifiedAdd' P1' P2' := (
@@ -29,7 +31,7 @@ Section Pre.
     let '(x2, y2) := P2' in
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
   ).
-  
+
   Lemma char_gt_2 : ZToField 2 <> (0: F q).
     intro; find_injection.
     pose proof two_lt_q.
@@ -38,7 +40,7 @@ Section Pre.
 
   Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
   Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
-  
+
   Ltac whatsNotZero :=
     repeat match goal with
     | [H: ?lhs = ?rhs |- _ ] =>
@@ -67,11 +69,11 @@ Section Pre.
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
     intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
-  
-    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
     destruct a_square as [sqrt_a a_square'].
     rewrite <-a_square' in *.
-  
+
     (* Furthermore... *)
     pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
     rewrite Hc2 in Heqt at 2.
@@ -80,7 +82,7 @@ Section Pre.
     rewrite Hcontra in Heqt.
     replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
     rewrite <-Hc1 in Heqt.
-  
+
     (* main equation for both potentially nonzero denominators *)
     destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
       try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
@@ -97,11 +99,11 @@ Section Pre.
             destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
         end
       end.
-  
+
     assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
-  
+
     replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
-  
+
     (* contradiction: product of nonzero things is zero *)
     destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
     destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
@@ -119,7 +121,7 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
       intro Hz; rewrite Hz in H; intuition.
   Qed.
-  
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) ->
     onCurve (x2, y2) ->
@@ -130,27 +132,27 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
       intro Hz; rewrite Hz in H; apply H; field.
   Qed.
-  
+
   Definition zeroOnCurve : onCurve (0, 1).
     simpl. field.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
     (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
     onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
   Proof.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
-      * c=1 and an extra a in front of x^2 *) 
-  
-    injection H; clear H; intros.
-  
+      * c=1 and an extra a in front of x^2 *)
+
+    injection H; cbv beta iota; clear H; intros.
+
     Ltac t x1 y1 x2 y2 :=
       assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
              = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
       assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
              = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
     t x1 y1 x2 y2; t x2 y2 x1 y1.
-  
+
     remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
       (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
     assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
@@ -158,7 +160,7 @@ Section Pre.
     (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
      y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
     replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-  
+
     match goal with [ |- ?x = 1 ] => replace x with
     ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
      ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
@@ -175,7 +177,7 @@ Section Pre.
       auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
         edwardsAddCompleteMinus, edwardsAddCompletePlus.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
     onCurve (unifiedAdd' P1 P2).
   Proof.
@@ -183,4 +185,4 @@ Section Pre.
     remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
     eapply unifiedAdd'_onCurve'; eauto.
   Qed.
-End Pre.
\ No newline at end of file
+End Pre.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index dabfcf883..6168f88bd 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -1,3 +1,4 @@
+Require Import Coq.omega.Omega.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.Pre.
 
@@ -10,7 +11,7 @@ Require Export Crypto.Util.IterAssocOp.
 
 Section ModularArithmeticPreliminaries.
   Context {m:Z}.
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm.
+  Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
 
   Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
   Proof.
@@ -19,20 +20,20 @@ Section ModularArithmeticPreliminaries.
     f_equal.
     eapply UIP_dec, Z.eq_dec.
   Qed.
-  
+
   Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
     intros a.
     pose (@opp_with_spec m) as H.
-    change (@opp m) with (proj1_sig H). 
+    change (@opp m) with (proj1_sig H).
     destruct H; eauto.
   Qed.
-  
+
   Lemma F_pow_spec : forall (a:F m),
       pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
   Proof.
     intros a.
     pose (@pow_with_spec m) as H.
-    change (@pow m) with (proj1_sig H). 
+    change (@pow m) with (proj1_sig H).
     destruct H; eauto.
   Qed.
 End ModularArithmeticPreliminaries.
@@ -81,7 +82,7 @@ Ltac eq_remove_proofs := lazymatch goal with
     assert (Q := F_eq a b);
     simpl in *; apply Q; clear Q
 end.
-            
+
 Ltac Fdefn :=
   intros;
   rewrite ?F_opp_spec;
@@ -217,7 +218,7 @@ Section FandZ.
       rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ;
       simpl; congruence.
   Qed.
-  
+
   Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->
                                      b mod m =  (- a)  mod m.
   Proof.
@@ -244,7 +245,7 @@ Section FandZ.
     intros.
     pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial.
   Qed.
-  
+
   Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.
   Proof.
     intros.
@@ -282,7 +283,7 @@ Section FandZ.
   Proof.
     Fdefn.
   Qed.
- 
+
   (* Compatibility between inject and pow *)
   Lemma ZToField_pow : forall x n,
     @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m).
@@ -317,7 +318,7 @@ End FandZ.
 
 Section RingModuloPre.
   Context {m:Z}.
-  Local Coercion ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm.
+  Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
   (* Substitution to prove all Compats *)
   Ltac compat := repeat intro; subst; trivial.
 
@@ -362,12 +363,12 @@ Section RingModuloPre.
   Proof.
     Fdefn; rewrite Z.mul_1_r; auto.
   Qed.
-    
+
   Lemma F_mul_assoc:
     forall x y z : F m, x * (y * z) = x * y * z.
   Proof.
     Fdefn.
-  Qed.  
+  Qed.
 
   Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
   Proof.
@@ -390,7 +391,7 @@ Section RingModuloPre.
   Qed.
 
   (***** Division Theory *****)
-  Definition Fquotrem(a b: F m): F m * F m := 
+  Definition Fquotrem(a b: F m): F m * F m :=
     let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m).
   Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.
   Proof.
@@ -434,7 +435,7 @@ Section RingModuloPre.
   Qed.
 
   (* Redefine our division theory under the ring morphism *)
-  Lemma Fmorph_div_theory: 
+  Lemma Fmorph_div_theory:
       div_theory eq Zplus Zmult (@ZToField m) Z.quotrem.
   Proof.
     constructor; intros; intuition.
@@ -451,7 +452,7 @@ Section RingModuloPre.
     Fdefn.
   Qed.
 End RingModuloPre.
-  
+
 Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
 Ltac Fexp_tac t := Ncst t.
 Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
@@ -470,49 +471,49 @@ Module RingModulo (Export M : Modulus).
   Definition ring_morph_modulo := @Fring_morph modulus.
   Definition morph_div_theory_modulo := @Fmorph_div_theory modulus.
   Definition power_theory_modulo := @Fpower_theory modulus.
-  
+
   Add Ring GFring_Z : ring_theory_modulo
     (morphism ring_morph_modulo,
      constants [Fconstant],
      div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]). 
+     power_tac power_theory_modulo [Fexp_tac]).
 End RingModulo.
 
 Section VariousModulo.
   Context {m:Z}.
-  
+
   Add Ring GFring_Z : (@Fring_theory m)
     (morphism (@Fring_morph m),
      constants [Fconstant],
      div (@Fmorph_div_theory m),
-     power_tac (@Fpower_theory m) [Fexp_tac]). 
+     power_tac (@Fpower_theory m) [Fexp_tac]).
 
   Lemma F_mul_0_l : forall x : F m, 0 * x = 0.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_mul_0_r : forall x : F m, x * 0 = 0.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
     intros; intuition; subst.
     assert (0 * b = 0) by ring; intuition.
   Qed.
-  
+
   Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
     intros; intuition; subst.
     assert (a * 0 = 0) by ring; intuition.
   Qed.
-  
+
   Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N ->
     (x ^ z) * (y ^ z) = (x * y) ^ z.
   Proof.
     intros.
     replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
-    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | 
+    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | |
       replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
     intros z' z'_nonneg IHz'.
     rewrite Z2N.inj_succ by auto.
@@ -521,7 +522,7 @@ Section VariousModulo.
     rewrite <- IHz'.
     ring.
   Qed.
-  
+
   Lemma F_opp_0 : opp (0 : F m) = 0%F.
   Proof.
     intros; ring.
@@ -563,7 +564,7 @@ Section VariousModulo.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z.
   Proof.
     intros ? ? ? A.
@@ -653,7 +654,7 @@ Section VariousModulo.
   Proof.
     split; intro A;
       [ replace w with (w - x + x) by ring
-      | replace w with (w + z - z) by ring ]; rewrite A; ring. 
+      | replace w with (w + z - z) by ring ]; rewrite A; ring.
   Qed.
 
   Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index bb6c68423..350660323 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -50,7 +50,7 @@ Section PseudoMersenneProofs.
   Qed.
 
   Lemma sub_rep : forall c c_0modq, (length c <= length base)%nat ->
-    forall u v x y, u ~= x -> v ~= y -> 
+    forall u v x y, u ~= x -> v ~= y ->
     ModularBaseSystem.sub c c_0modq u v ~= (x-y)%F.
   Proof.
     autounfold; unfold ModularBaseSystem.sub; intuition. {
@@ -66,7 +66,7 @@ Section PseudoMersenneProofs.
     subst; auto.
   Qed.
 
-  Lemma decode_short : forall (us : BaseSystem.digits), 
+  Lemma decode_short : forall (us : BaseSystem.digits),
     (length us <= length base)%nat ->
     BaseSystem.decode base us = BaseSystem.decode ext_base us.
   Proof.
@@ -80,11 +80,11 @@ Section PseudoMersenneProofs.
   Qed.
 
   Lemma mul_rep_extended : forall (us vs : BaseSystem.digits),
-      (length us <= length base)%nat -> 
+      (length us <= length base)%nat ->
       (length vs <= length base)%nat ->
       (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs).
   Proof.
-      intros. 
+      intros.
       rewrite mul_rep by (apply ExtBaseVector || unfold ext_base; simpl_list; omega).
       f_equal; rewrite decode_short; auto.
   Qed.
@@ -93,7 +93,7 @@ Section PseudoMersenneProofs.
     pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega.
   Qed.
 
-  (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *) 
+  (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *)
   Lemma pseudomersenne_add: forall x y, (x + ((2^k) * y)) mod modulus = (x + (c * y)) mod modulus.
   Proof.
     intros.
@@ -137,7 +137,7 @@ Section PseudoMersenneProofs.
     rewrite mul_each_rep; auto.
   Qed.
 
-  Lemma reduce_length : forall us, 
+  Lemma reduce_length : forall us,
       (length us <= length ext_base)%nat ->
       (length (reduce us) <= length base)%nat.
   Proof.
@@ -158,7 +158,7 @@ Section PseudoMersenneProofs.
     }
     assert ((length low <= length base)%nat)
       by (rewrite Heqlow; rewrite firstn_length; apply Min.le_min_l).
-    assert (length high <= length base)%nat 
+    assert (length high <= length base)%nat
       by (rewrite Heqhigh; rewrite map_length; rewrite skipn_length;
       rewrite extended_base_length in H; omega).
     rewrite add_trailing_zeros; auto.
@@ -185,7 +185,7 @@ Section PseudoMersenneProofs.
   Qed.
 
   Lemma set_nth_sum : forall n x us, (n < length us)%nat ->
-    BaseSystem.decode base (set_nth n x us) = 
+    BaseSystem.decode base (set_nth n x us) =
     (x - nth_default 0 us n) * nth_default 0 base n + BaseSystem.decode base us.
   Proof.
     intros.
@@ -213,7 +213,7 @@ Section PseudoMersenneProofs.
   Qed.
 
   Lemma add_to_nth_sum : forall n x us, (n < length us)%nat ->
-    BaseSystem.decode base (add_to_nth n x us) = 
+    BaseSystem.decode base (add_to_nth n x us) =
     x * nth_default 0 base n + BaseSystem.decode base us.
   Proof.
     unfold add_to_nth; intros; rewrite set_nth_sum; try ring_simplify; auto.
@@ -269,7 +269,7 @@ Section CarryProofs.
   Context `{prm : PseudoMersenneBaseParams}.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
   Hint Unfold log_cap.
-  
+
   Lemma base_length_lt_pred : (pred (length base) < length base)%nat.
   Proof.
     pose proof base_length_nonzero; omega.
@@ -283,7 +283,7 @@ Section CarryProofs.
     apply limb_widths_nonneg.
     eapply nth_error_value_In; eauto.
   Qed.
-    
+
   Lemma nth_default_base_succ : forall i, (S i < length base)%nat ->
     nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i.
   Proof.
@@ -637,7 +637,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma carry_unaffected_low : forall i j us, ((0 < i < j)%nat \/ (i = 0 /\ j <> 0 /\ j <> pred (length base))%nat)->
-    (length us = length base) -> 
+    (length us = length base) ->
     nth_default 0 (carry j us) i = nth_default 0 us i.
   Proof.
     intros.
@@ -652,7 +652,7 @@ Section CanonicalizationProofs.
           (omega || rewrite length_add_to_nth; rewrite length_set_nth; pose proof base_length_nonzero; omega).
         reflexivity.
   Qed.
-  
+
   Lemma carry_unaffected_high : forall i j us, (S j < i)%nat -> (length us = length base) ->
     nth_default 0 (carry j us) i = nth_default 0 us i.
   Proof.
@@ -669,7 +669,7 @@ Section CanonicalizationProofs.
     nth_default 0 (carry j us) i = nth_default 0 us i.
   Proof.
     unfold carry, carry_simple, carry_and_reduce; intros.
-    break_if; (add_set_nth; 
+    break_if; (add_set_nth;
       [ rewrite max_bound_shiftr_eq_0 by omega; ring
       | subst; apply pow2_mod_log_cap_small; assumption ]).
   Qed.
@@ -744,7 +744,7 @@ Section CanonicalizationProofs.
       fold (carry_sequence (make_chain j) us); carry_length_conditions.
   Qed.
 
-  Lemma carry_sequence_unaffected : forall i us j, (j < i)%nat -> (length us = length base)%nat -> 
+  Lemma carry_sequence_unaffected : forall i us j, (j < i)%nat -> (length us = length base)%nat ->
     nth_default 0 (carry_sequence (make_chain j) us) i = nth_default 0 us i.
   Proof.
     induction j; [simpl; intros; omega | ].
@@ -867,7 +867,7 @@ Section CanonicalizationProofs.
   Proof.
     unfold carry_full, full_carry_chain; intros.
     rewrite <- base_length.
-    replace (length base) with (S (pred (length base))) at 1 2 by omega.
+    replace (length base) with (S (pred (length base))) by omega.
     simpl.
     unfold carry, carry_and_reduce; break_if; try omega.
     clear_obvious; add_set_nth.
@@ -893,9 +893,9 @@ Section CanonicalizationProofs.
      - apply carry_bounds_lower; carry_length_conditions.
      - rewrite nth_default_out_of_bounds; carry_length_conditions.
   Qed.
- 
+
   (* END proofs about first carry loop *)
- 
+
   (* BEGIN proofs about second carry loop *)
 
   Lemma carry_sequence_carry_full_bounds_same : forall us i, pre_carry_bounds us ->
@@ -923,7 +923,7 @@ Section CanonicalizationProofs.
           rewrite <-max_bound_log_cap, <-Z.add_1_l.
           apply Z.add_lt_le_mono; omega.
         * eapply Z.le_lt_trans; [ apply IHi; auto; omega | ].
-          apply Z.lt_mul_diag_r; auto; omega. 
+          apply Z.lt_mul_diag_r; auto; omega.
       - rewrite carry_sequence_unaffected by carry_length_conditions.
         apply carry_full_bounds; auto; omega.
   Qed.
@@ -945,7 +945,7 @@ Section CanonicalizationProofs.
     + rewrite Z.add_comm.
       apply Z.add_le_mono.
       - apply carry_bounds_0_upper; carry_length_conditions.
-      - replace c with (c * 1) at 2 by ring.
+      - etransitivity; [ | replace c with (c * 1) by ring; reflexivity ].
         apply Z.mul_le_mono_pos_l; try omega.
         rewrite Z.shiftr_div_pow2 by auto.
         apply Z.div_le_upper_bound; auto.
@@ -968,9 +968,9 @@ Section CanonicalizationProofs.
     split.
     + zero_bounds. destruct i;
         [ simpl; pose proof (carry_full_2_bounds_0 us PCB length_eq); omega | ].
-      - rewrite carry_sequence_unaffected by carry_length_conditions.
-        apply carry_full_bounds; carry_length_conditions.
-        carry_seq_lower_bound.
+      rewrite carry_sequence_unaffected by carry_length_conditions.
+      apply carry_full_bounds; carry_length_conditions.
+      carry_seq_lower_bound.
     + rewrite <-max_bound_log_cap, <-Z.add_1_l.
       rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
       apply Z.add_le_mono.
@@ -1011,7 +1011,7 @@ Section CanonicalizationProofs.
     0 <= nth_default 0 (carry_sequence (make_chain (i + j)) (carry_full (carry_full us))) i <= max_bound i.
   Proof.
     induction j; intros; try omega.
-    split; (destruct j; [ rewrite Nat.add_1_r; simpl 
+    split; (destruct j; [ rewrite Nat.add_1_r; simpl
                          | rewrite <-plus_n_Sm; simpl; rewrite carry_unaffected_low by carry_length_conditions; eapply IHj; eauto; omega ]).
     + apply nth_default_carry_bound_lower; carry_length_conditions.
     + apply nth_default_carry_bound_upper; carry_length_conditions.
@@ -1041,7 +1041,7 @@ Section CanonicalizationProofs.
       add_set_nth.
       apply pow2_mod_log_cap_bounds_lower.
     + rewrite carry_unaffected_low by carry_length_conditions.
-      assert (0 < S i < length base)%nat by omega. 
+      assert (0 < S i < length base)%nat by omega.
       intuition.
   Qed.
 
@@ -1105,9 +1105,9 @@ Section CanonicalizationProofs.
       apply carry_carry_done_done; try solve [carry_length_conditions].
       assumption.
   Qed.
- 
+
   (* END proofs about second carry loop *)
- 
+
   (* BEGIN proofs about third carry loop *)
 
   Lemma carry_full_3_bounds : forall us i, pre_carry_bounds us ->
@@ -1134,7 +1134,7 @@ Section CanonicalizationProofs.
       intuition.
       - replace (max_bound 0) with (c + (max_bound 0 - c)) by ring.
         apply Z.add_le_mono; try assumption.
-        replace c with (c * 1) at 2 by ring.
+        etransitivity; [ | replace c with (c * 1) by ring; reflexivity ].
         apply Z.mul_le_mono_pos_l; try omega.
         rewrite Z.shiftr_div_pow2 by auto.
         apply Z.div_le_upper_bound; auto.
@@ -2106,4 +2106,4 @@ Section CanonicalizationProofs.
     intros; eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
 
-End CanonicalizationProofs.
\ No newline at end of file
+End CanonicalizationProofs.
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index 2978fdd42..fca5576b7 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArit
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Coq.Logic.EqdepFacts.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.omega.Omega.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
@@ -46,7 +47,7 @@ Defined.
 Definition mulmod m := fun a b => a * b mod m.
 Definition powmod_pos m := Pos.iter_op (mulmod m).
 Definition powmod m a x := match x with N0 => 1 mod m | Npos p => powmod_pos m p (a mod m) end.
-  
+
 Lemma mulmod_assoc:
   forall m x y z : Z, mulmod m x (mulmod m y z) = mulmod m (mulmod m x y) z.
 Proof.
@@ -144,7 +145,7 @@ Definition mod_inv_eucl (a m:Z) : Z.
                                  (match d with Z.pos _ =>  u | _ => -u end)
           end) mod m).
 Defined.
-  
+
 Lemma reduced_nonzero_pos:
   forall a m : Z, m > 0 -> a <> 0 -> a = a mod m -> 0 < a.
 Proof.
@@ -209,7 +210,7 @@ Proof.
     unfold mod_inv_eucl; simpl.
     lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
     auto.
-  - 
+  -
     destruct a.
     cbv [proj1_sig mod_inv_eucl_sig].
     rewrite Z.mul_comm.
@@ -217,4 +218,4 @@ Proof.
     rewrite mod_inv_eucl_correct; eauto.
     intro; destruct H0.
     eapply exist_reduced_eq. congruence.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index d6c7fa4b8..7d354ab3e 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -9,9 +9,9 @@ Section Mod24.
 
   (* Specify modulus *)
   Let q := 24.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [ring]. Similar boilerplate works for [field] if
   the modulus is prime . *)
@@ -21,7 +21,7 @@ Section Mod24.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
   Proof.
@@ -37,9 +37,9 @@ Section Modq.
 
   (* Set notations + - * / refer to F operations *)
   Local Open Scope F_scope.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [field]. Similar boilerplate works for [ring] if
   the modulus is not prime . *)
@@ -49,7 +49,7 @@ Section Modq.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
   Proof.
@@ -170,7 +170,7 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; try exact Fq_1_neq_0.
   Qed.
 
-  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, 
+  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
    ZQ <> 0 ->
    ZP <> 0 ->
    ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
@@ -187,4 +187,3 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; assumption.
   Qed.
 End TimesZeroParametricTestModule.
-
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 3348be1d9..2ad3877ac 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -5,6 +5,8 @@ Require Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.Spec.ModularArithmetic.
 Local Open Scope F_scope.
 
+Global Set Asymmetric Patterns.
+
 Class TwistedEdwardsParams := {
   q : BinInt.Z;
   a : F q;
@@ -19,7 +21,7 @@ Class TwistedEdwardsParams := {
 Module E.
   Section TwistedEdwardsCurves.
     Context {prm:TwistedEdwardsParams}.
-  
+
     (* Twisted Edwards curves with complete addition laws. References:
     * <https://eprint.iacr.org/2008/013.pdf>
     * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
@@ -27,20 +29,20 @@ Module E.
     *)
     Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
     Definition point := { P | onCurve P}.
-  
+
     Definition zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
-    
+
     Definition add' P1' P2' :=
       let '(x1, y1) := P1' in
       let '(x2, y2) := P2' in
         (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-  
+
     Definition add (P1 P2 : point) : point :=
       let 'exist P1' pf1 := P1 in
       let 'exist P2' pf2 := P2 in
       exist _ (add' P1' P2')
         (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
-  
+
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with
       | O => zero
@@ -48,7 +50,7 @@ Module E.
       end.
   End TwistedEdwardsCurves.
 End E.
-  
+
 Delimit Scope E_scope with E.
 Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope.
\ No newline at end of file
+Infix "*" := E.mul : E_scope.
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 76efe3d79..8ee07fe5d 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -26,8 +26,8 @@ Section FieldOperations.
   Context {m : BinInt.Z}.
 
   (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *)
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m.
-  
+  Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F.
+
   Definition add (a b:F m) : F m := ZToField (a + b).
   Definition mul (a b:F m) : F m := ZToField (a * b).
 
@@ -69,4 +69,4 @@ Infix "-" := sub : F_scope.
 Infix "/" := div : F_scope.
 Infix "^" := pow : F_scope.
 Notation "0" := (ZToField 0) : F_scope.
-Notation "1" := (ZToField 1) : F_scope.
\ No newline at end of file
+Notation "1" := (ZToField 1) : F_scope.
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 3b90b5cdf..377fb9592 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -245,7 +245,7 @@ Section Ed25519Frep.
   Local Ltac Let_In_unRep :=
     match goal with
     | [ |- appcontext G[Let_In (unRep ?x) ?f] ]
-      => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta
+      => let G' := context G[Let_In x (fun y => f (unRep y))] in change G'; cbv beta
     end.
 
 
@@ -578,4 +578,4 @@ Section Ed25519Frep.
       reflexivity. } Unfocus.
     reflexivity.
   Defined.
-End Ed25519Frep.
\ No newline at end of file
+End Ed25519Frep.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 8aaf8caf6..68278ce4c 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -132,7 +132,7 @@ Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F255
   destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
   destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
   let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
-  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]];
     destruct E as [? r]; cbv [proj1_sig].
   cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
 Qed.
@@ -164,7 +164,7 @@ Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F255
   destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
   destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
   let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
-  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]];
     destruct E as [? r]; cbv [proj1_sig].
   cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
 Qed.
@@ -174,7 +174,7 @@ Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F255
   destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
   destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
   let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
-  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]];
     destruct E as [? r]; cbv [proj1_sig].
   cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Testbit.v b/src/Testbit.v
index 264069587..2bfcc3df6 100644
--- a/src/Testbit.v
+++ b/src/Testbit.v
@@ -3,6 +3,7 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.BaseSystem Crypto.BaseSystemProofs.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Import Nat.
 
 Local Open Scope Z.
 
@@ -209,4 +210,4 @@ Lemma testbit_spec : forall n us base limb_width, (0 < limb_width)%nat ->
 Proof.
   intros.
   erewrite unfold_bits_testbit, unfold_bits_decode; eauto; omega.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index cf3ebf29c..2d1ab6c58 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -1,12 +1,12 @@
-Require Import Coq.Arith.Arith.
+Require Import Coq.Arith.Arith Coq.Arith.Max.
 
 Ltac case_max :=
   match goal with [ |- context[max ?x ?y] ] =>
       destruct (le_dec x y);
       match goal with
-        | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by
+        | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by
           (exact H)
-        | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite Max.max_l by
+        | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite max_l by
           (exact (le_Sn_le _ _ (not_le _ _ H)))
       end
   end.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 6116312e1..82d22046d 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -1,5 +1,7 @@
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Require Import Coq.NArith.NArith Coq.PArith.BinPosDef.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+
 Local Open Scope equiv_scope.
 
 Generalizable All Variables.
@@ -147,7 +149,7 @@ Section IterAssocOp.
     destruct (funexp (test_and_op n a) (x, acc) y) as [i acc'].
     simpl in IHy.
     unfold test_and_op.
-    destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity.
+    destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity.
   Qed.
 
   Lemma iter_op_termination : forall sc a bound,
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 59898be7a..bc2c8425b 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.
+Import Nat.
 
 Local Open Scope nat_scope.
 
@@ -77,4 +78,3 @@ Proof.
     [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
     | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
 Qed.
-
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 536566312..a5716fca4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr
 Require Import Coq.omega.Omega 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.
@@ -208,7 +209,7 @@ Proof.
   rewrite (le_plus_minus n m) at 1 by assumption.
   rewrite Nat2Z.inj_add.
   rewrite Z.pow_add_r by apply Nat2Z.is_nonneg.
-  rewrite <- Z.div_div by first 
+  rewrite <- Z.div_div by first
     [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega
     | apply Z.pow_pos_nonneg; omega ].
   rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega).
@@ -332,7 +333,7 @@ Qed.
     replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2).
     rewrite Z.div_add_l by omega.
     reflexivity.
-    replace 2 with (2 ^ 1) at 2 by auto.
+    change 2 with (2 ^ 1) at 2.
     rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega).
     f_equal. omega.
   Qed.
@@ -345,7 +346,7 @@ Qed.
     + unfold Z.ones.
       rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r.
       omega.
-    + intros. 
+    + intros.
       destruct (Z_lt_le_dec x n); try omega.
       intuition.
       left.
@@ -360,7 +361,7 @@ Qed.
     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_le_lt_eq_dec i n G1).
     + destruct (Z_shiftr_ones' a n G i G0); omega.
     + subst; rewrite Z.sub_diag.
       destruct (Z_eq_dec a 0).