Make the library 20% faster: [auto with *] is evil

I do hereby revoke the privilege of [intuition] to grab random hints
from random databases.  This privilege is reserved for
[debug_intuition], which comes with a warning about not being used in
production code.  This tactic is useful in conjunction with `Print Hint
*`, to discover what hint databases the hints were grabbed from.

(Suggestions for renaming [debug_intuition] welcome.)

Any file using [intuition] must [Require Export
Crypto.Util.FixCoqMistakes.].  It's possible we could lift this
restriction by compiling [FixCoqMistakes] separately, and passing along
`-require FixCoqMistakes` to Coq.  Should we do this?

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m29.54s | Total                                             | 4m33.13s || -1m03.59s
------------------------------------------------------------------------------------
0m03.75s | BaseSystemProofs                                  | 0m43.84s || -0m40.09s
0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m34.48s || +0m08.09s
0m03.04s | Util/ListUtil                                     | 0m11.18s || -0m08.14s
0m01.62s | ModularArithmetic/PrimeFieldTheorems              | 0m09.53s || -0m07.90s
0m00.87s | Util/NumTheoryUtil                                | 0m07.61s || -0m06.74s
0m01.61s | Encoding/PointEncodingPre                         | 0m06.93s || -0m05.31s
0m51.95s | Specific/GF25519                                  | 0m47.52s || +0m04.42s
0m12.30s | Experiments/SpecEd25519                           | 0m11.29s || +0m01.01s
0m09.22s | Specific/GF1305                                   | 0m08.17s || +0m01.05s
0m03.48s | CompleteEdwardsCurve/Pre                          | 0m04.77s || -0m01.28s
0m02.70s | Assembly/State                                    | 0m04.09s || -0m01.38s
0m01.55s | ModularArithmetic/ModularArithmeticTheorems       | 0m02.93s || -0m01.38s
0m01.16s | Assembly/Pseudize                                 | 0m02.34s || -0m01.17s
0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s
0m06.02s | Algebra                                           | 0m06.67s || -0m00.65s
0m05.90s | Experiments/GenericFieldPow                       | 0m06.68s || -0m00.77s
0m04.65s | WeierstrassCurve/Pre                              | 0m05.27s || -0m00.61s
0m03.93s | ModularArithmetic/Pow2BaseProofs                  | 0m03.94s || -0m00.00s
0m03.70s | ModularArithmetic/Tutorial                        | 0m03.85s || -0m00.14s
0m02.83s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.84s || -0m00.00s
0m02.74s | Experiments/EdDSARefinement                       | 0m01.80s || +0m00.94s
0m02.35s | Util/ZUtil                                        | 0m02.51s || -0m00.15s
0m01.86s | Assembly/Wordize                                  | 0m02.32s || -0m00.45s
0m01.23s | ModularArithmetic/ExtendedBaseVector              | 0m01.20s || +0m00.03s
0m01.21s | BaseSystem                                        | 0m01.63s || -0m00.41s
0m01.03s | Experiments/SpecificCurve25519                    | 0m00.98s || +0m00.05s
0m01.01s | ModularArithmetic/ModularBaseSystemProofs         | 0m01.11s || -0m00.10s
0m00.95s | ModularArithmetic/BarrettReduction/Z              | 0m01.38s || -0m00.42s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding    | 0m01.81s || -0m00.89s
0m00.85s | ModularArithmetic/ModularBaseSystemField          | 0m00.86s || -0m00.01s
0m00.82s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.79s || +0m00.02s
0m00.80s | Assembly/QhasmEvalCommon                          | 0m00.93s || -0m00.13s
0m00.73s | Spec/EdDSA                                        | 0m00.59s || +0m00.14s
0m00.72s | Util/Tuple                                        | 0m00.71s || +0m00.01s
0m00.70s | Util/IterAssocOp                                  | 0m00.72s || -0m00.02s
0m00.67s | Encoding/ModularWordEncodingTheorems              | 0m00.71s || -0m00.03s
0m00.66s | Assembly/Pipeline                                 | 0m00.64s || +0m00.02s
0m00.65s | Testbit                                           | 0m00.65s || +0m00.00s
0m00.65s | Assembly/PseudoConversion                         | 0m00.65s || +0m00.00s
0m00.64s | Util/AdditionChainExponentiation                  | 0m00.63s || +0m00.01s
0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.64s || -0m00.01s
0m00.63s | Assembly/Pseudo                                   | 0m00.65s || -0m00.02s
0m00.62s | ModularArithmetic/ModularBaseSystem               | 0m00.57s || +0m00.05s
0m00.61s | ModularArithmetic/ModularBaseSystemList           | 0m00.57s || +0m00.04s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.69s || -0m00.08s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.59s || +0m00.01s
0m00.56s | Assembly/StringConversion                         | 0m00.56s || +0m00.00s
0m00.54s | Spec/ModularWordEncoding                          | 0m00.61s || -0m00.06s
0m00.54s | Assembly/QhasmUtil                                | 0m00.46s || +0m00.08s
0m00.52s | Assembly/Qhasm                                    | 0m00.53s || -0m00.01s
0m00.48s | Assembly/AlmostQhasm                              | 0m00.52s || -0m00.04s
0m00.48s | ModularArithmetic/Pre                             | 0m00.48s || +0m00.00s
0m00.46s | Assembly/Vectorize                                | 0m00.72s || -0m00.25s
0m00.45s | Spec/WeierstrassCurve                             | 0m00.44s || +0m00.01s
0m00.44s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.00s
0m00.43s | ModularArithmetic/Pow2Base                        | 0m00.51s || -0m00.08s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.38s || +0m00.03s
0m00.41s | Spec/CompleteEdwardsCurve                         | 0m00.43s || -0m00.02s
0m00.34s | Spec/ModularArithmetic                            | 0m00.36s || -0m00.01s
0m00.03s | Util/FixCoqMistakes                               |   N/A    || +0m00.03s
0m00.02s | Util/Notations                                    | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics                                      | 0m00.02s || +0m00.00s

_CoqProject

@@ -64,6 +64,7 @@ src/Tactics/Algebra_syntax/Nsatz.v
 src/Util/AdditionChainExponentiation.v
 src/Util/CaseUtil.v
 src/Util/Decidable.v
+src/Util/FixCoqMistakes.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v

src/Algebra.v

@@ -5,6 +5,7 @@ Require Import Crypto.Util.Notations.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 Require Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.

src/Assembly/Pseudize.v

@@ -1,7 +1,8 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith NPeano List Sumbool Compare_dec Omega.
-Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State.
-Require Export Wordize Vectorize.
+Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.Lists.List Coq.Bool.Sumbool Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Pseudo Crypto.Assembly.State.
+Require Export Crypto.Assembly.Wordize Crypto.Assembly.Vectorize.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Import Pseudo ListNotations StateCommon EvalUtil ListState.
 
@@ -34,8 +35,8 @@ Section Conversion.
     replace (k mod n) with k by (
       assert (n <> 0) as NZ by omega;
       pose proof (Nat.div_mod k n NZ);
-      replace (k mod n) with (k - n * (k / n)) by intuition;
-      rewrite (Nat.div_small k n); intuition).
+      replace (k mod n) with (k - n * (k / n)) by intuition auto with zarith;
+      rewrite (Nat.div_small k n); intuition auto with zarith).
 
     autounfold; simpl.
     destruct (nth_error x k); simpl; try inversion H0; intuition.
@@ -48,8 +49,8 @@ Section Conversion.
     intros; autounfold; simpl.
     unfold indexize;
       destruct (le_dec n 0), (le_dec len 0);
-      try replace n with 0 in * by intuition;
-      try replace len with 0 in * by intuition;
+      try replace n with 0 in * by intuition auto with zarith;
+      try replace len with 0 in * by intuition auto with zarith;
       autounfold; simpl in *; rewrite H;
       autounfold; simpl; rewrite NToWord_wordToN;
       intuition.
@@ -247,7 +248,7 @@ Section Conversion.
       simpl; intuition.
   Qed.
 
-  Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := 
+  Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type :=
     {p: @Pseudo w s n m | forall x: (list (word w)),
       List.length x = n -> exists m' c',
       pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}.

src/Assembly/Pseudo.v

@@ -1,6 +1,7 @@
-Require Import QhasmCommon QhasmUtil State.
-Require Import Language QhasmEvalCommon.
-Require Import List Compare_dec Omega.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State.
+Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon.
+Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module Pseudo <: Language.
   Import EvalUtil ListState.
@@ -96,7 +97,7 @@ Module Pseudo <: Language.
           else pseudoEval r st ))
 
     | PFunExp n p e =>
-      (fix funexpseudo (e': nat) (st': ListState w) := 
+      (fix funexpseudo (e': nat) (st': ListState w) :=
         match e' with
         | O => Some st'
         | S e'' =>
@@ -116,7 +117,7 @@ Module Pseudo <: Language.
   Definition indexize {n: nat} (x: nat): Index n.
     intros; destruct (le_dec n 0).
 
-    - exists 0; abstract intuition.
+    - exists 0; abstract intuition auto with zarith.
     - exists (x mod n)%nat; abstract (
         pose proof (Nat.mod_bound_pos x n); omega).
   Defined.
@@ -179,4 +180,3 @@ Module Pseudo <: Language.
 
   Close Scope pseudo_notations.
 End Pseudo.
-

src/Assembly/QhasmEvalCommon.v

@@ -1,7 +1,8 @@
-Require Import QhasmCommon QhasmUtil State.
-Require Import ZArith Sumbool.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State.
+Require Import Coq.ZArith.ZArith Coq.Bool.Sumbool.
 Require Import Bedrock.Word.
-Require Import Logic.Eqdep_dec ProofIrrelevance.
+Require Import Coq.Logic.Eqdep_dec Coq.Logic.ProofIrrelevance.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module EvalUtil.
   Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
@@ -78,13 +79,13 @@ Module EvalUtil.
   Proof. induction a; unfold getWidth; simpl; intuition. Qed.
 
   Lemma width_eq {n} (a b: Width n): a = b.
-  Proof. 
+  Proof.
     assert (Some a = Some b) as H by (
       replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition);
       replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition);
       intuition).
     inversion H; intuition.
-  Qed. 
+  Qed.
 
   (* Mapping Conversions *)
 
@@ -102,29 +103,29 @@ Module EvalUtil.
 
   Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}.
     refine (match (a, b) as p' return (a, b) = p' -> _ with
-    | (regM v, regM v') => fun _ => 
+    | (regM v, regM v') => fun _ =>
         if (Nat.eq_dec (regName v) (regName v'))
         then left _
         else right _
 
-    | (stackM v, stackM v') => fun _ => 
+    | (stackM v, stackM v') => fun _ =>
         if (Nat.eq_dec (stackName v) (stackName v'))
         then left _
         else right _
 
-    | (constM v, constM v') => fun _ => 
+    | (constM v, constM v') => fun _ =>
         if (Nat.eq_dec (constValueN v) (constValueN v'))
         then left _
         else right _
 
-    | (memM _ v i, memM _ v' i') => fun _ => 
-        if (Nat.eq_dec (memName v) (memName v')) 
+    | (memM _ v i, memM _ v' i') => fun _ =>
+        if (Nat.eq_dec (memName v) (memName v'))
         then if (Nat.eq_dec (memLength v) (memLength v'))
         then if (Nat.eq_dec (proj1_sig i) (proj1_sig i'))
         then left _ else right _ else right _ else right _
 
     | _ => fun _ => right _
-    end (eq_refl (a, b))); 
+    end (eq_refl (a, b)));
       try destruct v, v'; subst;
       unfold regName, stackName, constValueN, memName, memLength in *;
       repeat progress (try apply f_equal; subst; match goal with
@@ -158,10 +159,10 @@ Module EvalUtil.
       | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] =>
         let l0 := fresh in let l1 := fresh in
         destruct a, b; simpl in H; subst
-      | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => 
+      | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] =>
         apply (inj_pair2_eq_dec _ Nat.eq_dec) in H;
             subst; intuition
-      | [ H: exist _ _ _ = exist _ _ _ |- _ ] => 
+      | [ H: exist _ _ _ = exist _ _ _ |- _ ] =>
         inversion H; subst; intuition
 
         (* Single specialized wordToNat proof *)
@@ -176,12 +177,12 @@ Module EvalUtil.
 
   Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
     assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true})
-      by abstract (destruct (a <? b)%nat; intuition);
+      by abstract (destruct (a <? b)%nat; intuition auto with bool);
       destruct H.
 
     - left; abstract (apply Nat.ltb_lt; intuition).
 
-    - right; abstract (rewrite Nat.ltb_lt in *; intuition).
+    - right; abstract (rewrite Nat.ltb_lt in *; intuition auto with zarith).
   Defined.
 
   Fixpoint stackNames {n} (lst: list (Mapping n)): list nat :=
@@ -216,12 +217,12 @@ Module QhasmEval.
       omap (getReg r state) (fun v =>
         if (Nat.eq_dec O (wordToNat v))
         then Some true
-        else Some false) 
+        else Some false)
     | CReg n o a b =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
           Some (evalTest o va vb)))
-    | CConst n o a c => 
+    | CConst n o a c =>
       omap (getReg a state) (fun va =>
         Some (evalTest o va (constValueW c)))
     end.
@@ -245,51 +246,51 @@ Module QhasmEval.
             let (v', co) := (evalIntOp o va vb) in
             Some (setCarryOpt co (setReg a v' state))))
 
-    | IOpMem _ _ o r m i => 
+    | IOpMem _ _ o r m i =>
       omap (getReg r state) (fun va =>
         omap (getMem m i state) (fun vb =>
             let (v', co) := (evalIntOp o va vb) in
             Some (setCarryOpt co (setReg r v' state))))
 
-    | DOp _ o a b (Some x) => 
+    | DOp _ o a b (Some x) =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             let (low, high) := (evalDualOp o va vb) in
             Some (setReg x high (setReg a low state))))
 
-    | DOp _ o a b None => 
+    | DOp _ o a b None =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             let (low, high) := (evalDualOp o va vb) in
             Some (setReg a low state)))
 
-    | ROp _ o r i => 
+    | ROp _ o r i =>
       omap (getReg r state) (fun v =>
         let v' := (evalRotOp o v i) in
         Some (setReg r v' state))
 
-    | COp _ o a b => 
+    | COp _ o a b =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             match (getCarry state) with
             | None => None
-            | Some c0 => 
+            | Some c0 =>
             let (v', c') := (evalCarryOp o va vb c0) in
             Some (setCarry c' (setReg a v' state))
             end))
     end.
 
   Definition evalAssignment (a: Assignment) (state: State): option State :=
     match a with
-    | ARegMem _ _ r m i => 
+    | ARegMem _ _ r m i =>
       omap (getMem m i state) (fun v => Some (setReg r v state))
     | AMemReg _ _ m i r =>
       omap (getReg r state) (fun v => Some (setMem m i v state))
     | AStackReg _ a b =>
       omap (getReg b state) (fun v => Some (setStack a v state))
     | ARegStack _ a b =>
       omap (getStack b state) (fun v => Some (setReg a v state))
-    | ARegReg _ a b => 
+    | ARegReg _ a b =>
       omap (getReg b state) (fun v => Some (setReg a v state))
     | AConstInt _ r c =>
       Some (setReg r (constValueW c) state)

src/Assembly/QhasmUtil.v

@@ -1,6 +1,7 @@
-Require Import ZArith NArith NPeano.
-Require Import QhasmCommon.
+Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano.
+Require Import Crypto.Assembly.QhasmCommon.
 Require Export Bedrock.Word.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Delimit Scope nword_scope with w.
 Local Open Scope nword_scope.
@@ -14,12 +15,12 @@ Section Util.
 
   Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
     refine (split1 k (n - k) (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
+    abstract (replace n with (k + (n - k)) by omega; intuition auto with arith).
   Defined.
 
   Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
     refine (split2 (n - k) k (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
+    abstract (replace n with (k + (n - k)) by omega; intuition auto with zarith).
   Defined.
 
   Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
@@ -61,7 +62,7 @@ Section Util.
     refine match (le_dec m n) with
     | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
     | right p => (extend _ x, _)
-    end; try abstract intuition.
+    end; try abstract intuition auto with zarith.
 
     replace (n - m) with O by abstract omega; exact WO.
   Defined.
@@ -75,4 +76,4 @@ Section Util.
   Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
 End Util.
 
-Close Scope nword_scope.
+Close Scope nword_scope.

src/Assembly/State.v

@@ -1,12 +1,14 @@
-Require Export String List Logic.
+Require Export Coq.Strings.String Coq.Lists.List Coq.Init.Logic.
 Require Export Bedrock.Word.
 
-Require Import ZArith NArith NPeano Ndec.
-Require Import Compare_dec Omega.
-Require Import OrderedType Coq.Structures.OrderedTypeEx.
-Require Import FMapPositive FMapFullAVL JMeq.
+Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec.
+Require Import Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx.
+Require Import Coq.FSets.FMapPositive Coq.FSets.FMapFullAVL Coq.Logic.JMeq.
 
-Require Import QhasmUtil QhasmCommon.
+Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmCommon.
+
+Require Export Crypto.Util.FixCoqMistakes.
 
 (* We want to use pairs and triples as map keys: *)
 
@@ -50,16 +52,16 @@ Module Pair_as_OT <: UsualOrderedType.
       destruct (Nat_as_OT.compare x0 y0);
       unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
 
-    - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+    - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition auto with zarith).
 
     - destruct (Nat_as_OT.compare x1 y1);
         unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
 
       + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
-      + apply EQ; abstract (unfold lt; simpl; subst; intuition).
-      + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+      + apply EQ; abstract (unfold lt; simpl; subst; intuition auto with crelations).
+      + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith).
 
-    - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+    - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith).
   Defined.
 
   Definition eq_dec (a b: t): {a = b} + {a <> b}.
@@ -69,14 +71,14 @@ Module Pair_as_OT <: UsualOrderedType.
     - right; abstract (
         unfold lt in *; simpl in *;
         destruct (Nat.eq_dec a0 b0); intuition;
-        inversion H; intuition).
+        inversion H; intuition auto with zarith).
 
     - left; abstract (inversion e; intuition).
 
     - right; abstract (
         unfold lt in *; simpl in *;
         destruct (Nat.eq_dec b0 a0); intuition;
-        inversion H; intuition).
+        inversion H; intuition auto with zarith).
   Defined.
 End Pair_as_OT.
 
@@ -132,7 +134,7 @@ Module Triple_as_OT <: UsualOrderedType.
       unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *;
       destruct (Nat.eq_dec (get0 x) (get0 y));
       destruct (Nat.eq_dec (get1 x) (get1 y));
-      simpl; intuition).
+      simpl; intuition auto with zarith).
 
   Ltac compare_eq x y :=
     abstract (
@@ -163,14 +165,14 @@ Module Triple_as_OT <: UsualOrderedType.
     - right; abstract (
         unfold lt, get0, get1, get2 in *; simpl in *;
         destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1);
-        intuition; inversion H; intuition).
+        intuition; inversion H; intuition auto with zarith).
 
     - left; abstract (inversion e; intuition).
 
     - right; abstract (
         unfold lt, get0, get1, get2 in *; simpl in *;
         destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1);
-        intuition; inversion H; intuition).
+        intuition; inversion H; intuition auto with zarith).
   Defined.
 End Triple_as_OT.
 

src/Assembly/Vectorize.v

@@ -1,6 +1,8 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
-Require Import ProofIrrelevance Ring List Omega.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.Arith.Compare_dec Coq.Arith.Arith.
+Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Coq.omega.Omega.
+
+Require Export Crypto.Util.FixCoqMistakes.
 
 Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x :=
   let y := x in f y.