Factor out fsatz lemmas

After    | File Name                   | Before   || Change    | % Change
-------------------------------------------------------------------------
1m11.42s | Total                       | 1m53.75s || -0m42.33s | -37.21%
-------------------------------------------------------------------------
1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96%
0m05.40s | Util/FsatzAutoLemmas        |   N/A    || +0m05.40s | ∞

3 files changed, 499 insertions, 242 deletions

diff --git a/_CoqProject b/_CoqProject
index 48f29bdab..926df76fa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5829,6 +5829,7 @@ src/Util/FixCoqMistakes.v
 src/Util/FixedWordSizes.v
 src/Util/FixedWordSizesEquality.v
 src/Util/ForLoop.v
+src/Util/FsatzAutoLemmas.v
 src/Util/GlobalSettings.v
 src/Util/HList.v
 src/Util/HProp.v
diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v
index 06d9a48ec..a44ac7159 100644
--- a/src/Curves/Weierstrass/Jacobian.v
+++ b/src/Curves/Weierstrass/Jacobian.v
@@ -8,6 +8,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SetoidSubst.
 Require Import Crypto.Util.Notations Crypto.Util.LetIn.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.Sigma.
+Require Import Crypto.Util.FsatzAutoLemmas.
 
 Module Jacobian.
   Section Jacobian.
@@ -191,254 +192,264 @@ Module Jacobian.
         find_and_do_or_prove_by_fsatz ty ltac:(fun H' => apply H' in H0; [ | exact H1 ]).
       Local Ltac find_and_apply_or_prove_by_fsatz' H ty preapp :=
         find_and_do_or_prove_by_fsatz ty ltac:(fun H' => let H' := preapp H' in apply H' in H).
-      Local Ltac speed_up_fsatz :=
-        let fld := guess_field in
-        divisions_to_inverses fld;
-        repeat match goal with
-               | [ H : False |- _ ] => solve [ exfalso; exact H ]
-               | [ H : ?T |- ?T ] => exact H
-               | [ H : ?x <> ?x |- _ ] => solve [ exfalso; apply H; reflexivity ]
-               | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => solve [ exfalso; apply H', H ]
-               | [ H : ?x = 0 |- ?x * ?y <> 0 ] => exfalso
-               | [ H : ?y = 0 |- ?x * ?y <> 0 ] => exfalso
-               | [ H : ~?T |- ?T ] => exfalso
-               | [ H : ?T |- ~?T ] => exfalso
-               | [ H : ?x - ?x = 0 |- _ ] => clear H
-               | [ H : ?x * ?y = 0, H' : ?x = 0 |- _ ] => clear H
-               | [ H : ?x * ?y = 0, H' : ?y = 0 |- _ ] => clear H
-               | [ H : ?x = Fopp ?x |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a, a = Fopp a -> a = 0)
-               | [ H : ?x <> Fopp ?x |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a, a <> Fopp a -> a <> 0)
-               | [ H : ?x + ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall y, y + y = 0 -> y = 0)
-               | [ H : Finv (?x^3) = 0, H' : ?x <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a, Finv (a^3) = 0 -> a <> 0 -> False)
-               | [ H : ?x - ?y = 0, H' : ?y <> ?x |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a - b = 0 -> b = a)
-               | [ H : ?x - ?y = 0, H' : ?x <> ?y |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a - b = 0 -> a = b)
-               | [ H : ?x * ?y * ?z <> 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b c, a * b * c <> 0 -> a * c <> 0)
-               | [ H : ?x * ?y^3 <> 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a * b <> 0 -> a <> 0)
-               | [ H : ?x * ?y^2 <> 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a * b <> 0 -> a <> 0)
-               | [ H : ?x^2 - ?y^2 = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a^2 - b^2 = 0 -> (a - b) * (a + b) = 0)
-               | [ H : ?x + ?y * ?z = 0, H' : ?x <> Fopp (?z * ?y) |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a + b * c = 0 -> a <> Fopp (c * b) -> False)
-               | [ H : ?x + ?x <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a, a + a <> 0 -> a <> 0)
-               | [ H : ?x - ?y <> 0, H' : ?y = ?x |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a - b <> 0 -> b <> a)
-               | [ H : ?x - ?y <> 0, H' : ?x = ?y |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a - b <> 0 -> a <> b)
-               | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - (a^2 + b^2) = 0 -> a * b = 0)
-               | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - (a^2 + b^2) <> 0 -> a * b <> 0)
-               | [ H : ?x * ?y = 0, H' : ?x <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b, a * b = 0 -> a <> 0 -> b = 0)
-               | [ H : ?x * ?y = 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b, a * b = 0 -> b <> 0 -> a = 0)
-               | [ H : ?x * ?y <> 0, H' : ?x <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a * b <> 0 -> b <> 0)
-               | [ H : ?x * ?y <> 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, a * b <> 0 -> a <> 0)
-               | [ H : ?x * ?y <> 0, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b, a * b <> 0 -> a = 0 -> False)
-               | [ H : ?x * ?y <> 0, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b, a * b <> 0 -> b = 0 -> False)
-               | [ |- (?x + ?y)^2 - (?x^2 + ?y^2) = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a * b = 0 -> (a + b)^2 - (a^2 + b^2) = 0)
-               | [ |- (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a * b <> 0 -> (a + b)^2 - (a^2 + b^2) <> 0)
-               | [ |- (?x + ?y)^2 - ?x^2 - ?y^2 = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a * b = 0 -> (a + b)^2 - a^2 - b^2 = 0)
-               | [ |- (?x + ?y)^2 - ?x^2 - ?y^2 <> 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a * b <> 0 -> (a + b)^2 - a^2 - b^2 <> 0)
-               | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - (a^2 + b^2) = 0 -> a * b = 0)
-               | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - (a^2 + b^2) <> 0 -> a * b <> 0)
-               | [ H : (?x + ?y)^2 - ?x^2 - ?y^2 = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - a^2 - b^2 = 0 -> a * b = 0)
-               | [ H : (?x + ?y)^2 - ?x^2 - ?y^2 <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b, (a + b)^2 - a^2 - b^2 <> 0 -> a * b <> 0)
-               | [ H : ?x = 0 |- ?x * ?y = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a = 0 -> a * b = 0)
-               | [ H : ?y = 0 |- ?x * ?y = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, b = 0 -> a * b = 0)
-               | [ H : ?x <> 0 |- ?x * ?y <> 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a <> 0 -> b <> 0 -> a * b <> 0)
-               | [ H : ?y <> 0 |- ?x * ?y <> 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a <> 0 -> b <> 0 -> a * b <> 0)
-               | [ H : ?x <> 0 |- ?x * ?y = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, b = 0 -> a * b = 0)
-               | [ H : ?y <> 0 |- ?x * ?y = 0 ]
-                 => find_and_goal_apply_or_prove_by_fsatz (forall a b, a = 0 -> a * b = 0)
+      Local Ltac speed_up_fsatz_step_on pkg :=
+        let goal_if_var_neq_zero (* we want to keep lazymatch below, so we hack backtracking on is_var *)
+            := match goal with
+               | [ |- ?x <> 0 ] => let test := match goal with _ => is_var x end in
+                                   constr:(x <> 0)
+               | _ => I
+               end in
+        lazymatch goal with
+        | [ H : False |- _ ] => solve [ exfalso; exact H ]
+        | [ H : ?T |- ?T ] => exact H
+        | [ H : ?x <> ?x |- _ ] => solve [ exfalso; apply H; reflexivity ]
+        | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => solve [ exfalso; apply H', H ]
+        | [ H : ?x = 0 |- ?x * ?y <> 0 ] => exfalso
+        | [ H : ?y = 0 |- ?x * ?y <> 0 ] => exfalso
+        | [ H : ~?T |- ?T ] => exfalso
+        | [ H : ?T |- ~?T ] => exfalso
+        | [ H : ?x - ?x = 0 |- _ ] => clear H
+        | [ H : ?x * ?y = 0, H' : ?x = 0 |- _ ] => clear H
+        | [ H : ?x * ?y = 0, H' : ?y = 0 |- _ ] => clear H
+        | [ |- goal_if_var_neq_zero ] => intro
+        | [ H : ?x = Fopp ?x |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a, a = Fopp a -> a = 0)
+        | [ H : ?x <> Fopp ?x |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a, a <> Fopp a -> a <> 0)
+        | [ H : ?x + ?x = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall y, y + y = 0 -> y = 0)
+        | [ H : Finv (?x^3) = 0, H' : ?x <> 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a, Finv (a^3) = 0 -> a <> 0 -> False)
+        | [ H : ?x - ?y = 0, H' : ?y <> ?x |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a - b = 0 -> b = a)
+        | [ H : ?x - ?y = 0, H' : ?x <> ?y |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a - b = 0 -> a = b)
+        | [ H : ?x * ?y * ?z <> 0, H' : ?y <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c, a * b * c <> 0 -> a * c <> 0)
+        | [ H : ?x * ?y^3 <> 0, H' : ?y <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> a <> 0)
+        | [ H : ?x * ?y^2 <> 0, H' : ?y <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> a <> 0)
+        | [ H : ?x^2 - ?y^2 = ?z |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c, a^2 - b^2 = c -> (a - b) * (a + b) = c)
+        | [ H : ?x + ?y * ?z = 0, H' : ?x <> Fopp (?z * ?y) |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a + b * c = 0 -> a <> Fopp (c * b) -> False)
+        | [ H : ?x + ?x <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a, a + a <> 0 -> a <> 0)
+        | [ H : ?x - ?y <> 0, H' : ?y = ?x |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a - b <> 0 -> b <> a)
+        | [ H : ?x - ?y <> 0, H' : ?x = ?y |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a - b <> 0 -> a <> b)
+        | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - (a^2 + b^2) = 0 -> a * b = 0)
+        | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - (a^2 + b^2) <> 0 -> a * b <> 0)
+        | [ H : ?x * ?y = 0, H' : ?x <> 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b, a * b = 0 -> a <> 0 -> b = 0)
+        | [ H : ?x * ?y = 0, H' : ?y <> 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b, a * b = 0 -> b <> 0 -> a = 0)
+        | [ H : ?x * ?y <> 0, H' : ?x <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> b <> 0)
+        | [ H : ?x * ?y <> 0, H' : ?y <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> a <> 0)
+        | [ H : ?x * ?y <> 0, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> a <> 0)
+        | [ H : ?x * ?y <> 0, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, a * b <> 0 -> b <> 0)
+        | [ |- (?x + ?y)^2 - (?x^2 + ?y^2) = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a * b = 0 -> (a + b)^2 - (a^2 + b^2) = 0)
+        | [ |- (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a * b <> 0 -> (a + b)^2 - (a^2 + b^2) <> 0)
+        | [ |- (?x + ?y)^2 - ?x^2 - ?y^2 = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a * b = 0 -> (a + b)^2 - a^2 - b^2 = 0)
+        | [ |- (?x + ?y)^2 - ?x^2 - ?y^2 <> 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a * b <> 0 -> (a + b)^2 - a^2 - b^2 <> 0)
+        | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - (a^2 + b^2) = 0 -> a * b = 0)
+        | [ H : (?x + ?y)^2 - (?x^2 + ?y^2) <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - (a^2 + b^2) <> 0 -> a * b <> 0)
+        | [ H : (?x + ?y)^2 - ?x^2 - ?y^2 = 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - a^2 - b^2 = 0 -> a * b = 0)
+        | [ H : (?x + ?y)^2 - ?x^2 - ?y^2 <> 0 |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b, (a + b)^2 - a^2 - b^2 <> 0 -> a * b <> 0)
+        | [ H : ?x = 0 |- ?x * ?y = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a = 0 -> a * b = 0)
+        | [ H : ?y = 0 |- ?x * ?y = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, b = 0 -> a * b = 0)
+        | [ H : ?x <> 0 |- ?x * ?y <> 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a <> 0 -> b <> 0 -> a * b <> 0)
+        | [ H : ?y <> 0 |- ?x * ?y <> 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a <> 0 -> b <> 0 -> a * b <> 0)
+        | [ H : ?x <> 0 |- ?x * ?y = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, b = 0 -> a * b = 0)
+        | [ H : ?y <> 0 |- ?x * ?y = 0 ]
+          => F.goal_apply_lemma_on pkg (forall a b, a = 0 -> a * b = 0)
 
-               | [ H : ?x - ?y * ?z <> ?w, H' : ?y = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a - b * c <> d -> b = 1 -> a - c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x - ?y * ?z = ?w, H' : ?y = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a - b * c = d -> b = 1 -> a - c = d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x - ?y * ?z * ?w <> ?v, H' : ?y = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d e, a - b * c * d <> e -> b = 1 -> a - c * d <> e) ltac:(fun H'' => constr:(fun Hv => H'' x y z w v Hv H'))
-               | [ H : ?x - ?y * ?z * ?w = ?v, H' : ?y = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d e, a - b * c * d = e -> b = 1 -> a - c * d = e) ltac:(fun H'' => constr:(fun Hv => H'' x y z w v Hv H'))
-               | [ H : ?x - ?y * ?z^2 <> ?w, H' : ?z = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a - b * c^2 <> d -> c = 1 -> a - b <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x - ?y * ?z^2 = ?w, H' : ?z = 1 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a - b * c^2 = d -> c = 1 -> a - b = d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x - ?y * ?z <> ?w, H' : ?y = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a - b * c <> d -> b = 1 -> a - c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x - ?y * ?z = ?w, H' : ?y = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a - b * c = d -> b = 1 -> a - c = d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x - ?y * ?z * ?w <> ?v, H' : ?y = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d e, a - b * c * d <> e -> b = 1 -> a - c * d <> e) ltac:(fun H'' => constr:(fun Hv => H'' x y z w v Hv H'))
+        | [ H : ?x - ?y * ?z * ?w = ?v, H' : ?y = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d e, a - b * c * d = e -> b = 1 -> a - c * d = e) ltac:(fun H'' => constr:(fun Hv => H'' x y z w v Hv H'))
+        | [ H : ?x - ?y * ?z^2 <> ?w, H' : ?z = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a - b * c^2 <> d -> c = 1 -> a - b <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x - ?y * ?z^2 = ?w, H' : ?z = 1 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a - b * c^2 = d -> c = 1 -> a - b = d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
 
-               | [ H : ?x - ?y + ?z <> ?w, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a - b + c <> d -> b = 0 -> a + c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x - ?y <> ?z, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a - b <> c -> b = 0 -> a <> c) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y + ?z <> ?w, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * b + c <> d -> a = 0 -> c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x * ?y + ?z <> ?w, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * b + c <> d -> b = 0 -> c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
-               | [ H : ?x * ?y <> ?z, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b <> c -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y <> ?z, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b <> c -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : Fopp (?x * ?y) <> ?z, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, Fopp (a * b) <> c -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : Fopp (?x * ?y) <> ?z, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, Fopp (a * b) <> c -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y^3 = ?z, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a * b^3 = c -> b = 0 -> c = 0)
-               | [ H : ?x * ?y = ?z, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a * b = c -> a = 0 -> c = 0)
-               | [ H : ?x * ?y - ?z <> 0, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b - c <> 0 -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y - ?z <> 0, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b - c <> 0 -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y - ?z = 0, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b - c = 0 -> a = 0 -> c = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * ?y - ?z = 0, H' : ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a * b - c = 0 -> b = 0 -> c = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x - ?y * ?z = 0, H' : ?z = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a - b * c = 0 -> c = 0 -> a = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
-               | [ H : ?x * (?y * ?y^2) - ?z <> ?w |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b c d, a * (b * b^2) - c <> d -> a * (b^3) - c <> d)
-               | [ H : ?x * (?y * ?y^2) - ?z = ?w |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b c d, a * (b * b^2) - c = d -> a * (b^3) - c = d)
-               | [ H : ?x - (?y * ?y^2) * ?z <> ?w |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b c d, a - (b * b^2) * c <> d -> a - (b^3) * c <> d)
-               | [ H : ?x - (?y * ?y^2) * ?z = ?w |- _ ]
-                 => find_and_apply_or_prove_by_fsatz H (forall a b c d, a - (b * b^2) * c = d -> a - (b^3) * c = d)
-               | [ H : ?x * (?y * ?y^2) = 0, H' : ?y <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b, a * (b * b^2) = 0 -> b <> 0 -> a = 0)
-               | [ H : ?x * (?y * ?z) = 0, H' : ?z <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, c <> 0 -> a * (b * c) = 0 -> a * b = 0) ltac:(fun lem => constr:(lem x y z H'))
-               | [ H : ?x * ?y + ?z = 0, H' : ?x = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c, a = 0 -> a * b + c = 0 -> c = 0) ltac:(fun lem => constr:(lem x y z H'))
-               | [ H : ?x / ?y^3 = Fopp (?z / ?w^3), H' : ?y <> 0, H'' : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, c <> 0 -> d <> 0 -> a / c^3 = Fopp (b / d^3) -> a * d^3 + b * c^3 = 0) ltac:(fun lem => constr:(lem x z y w H' H''))
-               | [ H : ?x / ?y^3 <> Fopp (?z / ?w^3), H' : ?y <> 0, H'' : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, c <> 0 -> d <> 0 -> a / c^3 <> Fopp (b / d^3) -> a * d^3 + b * c^3 <> 0) ltac:(fun lem => constr:(lem x z y w H' H''))
-               | [ H : ?x / ?y^2 = ?z / ?w^2, H' : ?y <> 0, H'' : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, c <> 0 -> d <> 0 -> a / c^2 = b / d^2 -> a * d^2 - b * c^2 = 0) ltac:(fun lem => constr:(lem x z y w H' H''))
-               | [ H : ?x / ?y^2 <> ?z / ?w^2, H' : ?y <> 0, H'' : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, c <> 0 -> d <> 0 -> a / c^2 <> b / d^2 -> a * d^2 - b * c^2 <> 0) ltac:(fun lem => constr:(lem x z y w H' H''))
-               | [ H : ?x * (?y * ?y^2) - ?z * ?z^2 * ?w = 0, H' : ?x * ?y^3 + ?w * ?z^3 = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * b^3 + d * c^3 = 0 -> a * (b * b^2) - c * c^2 * d = 0 -> a * b^3 = 0) ltac:(fun lem => constr:(lem x y z w H'))
-               | [ H : ?x * Finv (?y^2) <> ?z * Finv (?w^2), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * Finv (b^2) <> c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) <> c * (b^2)) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
-               | [ H : ?x * Finv (?y^2) = ?z * Finv (?w^2), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * Finv (b^2) = c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) = c * (b^2)) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
-               | [ H : ?x * Finv (?y^3) = Fopp (?z * Finv (?w^3)), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * Finv (b^3) = Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) = Fopp (c * (b^3))) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
-               | [ H : ?x * Finv (?y^3) <> Fopp (?z * Finv (?w^3)), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall a b c d, a * Finv (b^3) <> Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) <> Fopp (c * (b^3))) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
-               | [ H : ?x = Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a = Fopp (b * c) -> a - c * b = 0 -> a = 0)
-               | [ H : ?x = Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a = Fopp (b * c) -> a - c * b = 0 -> a = 0)
-               | [ H : ?x <> Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a <> Fopp (b * c) -> a - c * b = 0 -> a * b * c <> 0)
-               | [ H : ?x <> Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
-                 => find_and_apply_or_prove_by_fsatz2 H H' (forall a b c, a <> Fopp (b * c) -> a - c * b = 0 -> a * b * c <> 0)
-               | [ H : ?y^2 = ?c^3 + ?a * ?c * (?x^2)^2 + ?b * (?x^3)^2,
-                       H' : ?y'^2 = ?c'^3 + ?a * ?c' * (?x'^2)^2 + ?b * (?x'^3)^2,
-                            H0 : ?c' * ?x^2 - ?c * ?x'^2 = 0
-                   |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall X Y X' Y' A B C C', Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 - C * X'^2 = 0 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0) ltac:(fun Hv => constr:(fun H => Hv x y x' y' a b c c' H H' H0))
-               | [ H : ?y^2 = ?c^3 + ?a * ?c * (?x^2)^2 + ?b * (?x^3)^2,
-                       H' : ?y'^2 = ?c'^3 + ?a * ?c' * (?x'^2)^2 + ?b * (?x'^3)^2,
-                            H0 : ?c' * ?x^2 = ?c * ?x'^2
-                   |- _ ]
-                 => find_and_apply_or_prove_by_fsatz' H (forall X Y X' Y' A B C C', Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 = C * X'^2 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0) ltac:(fun Hv => constr:(fun H => Hv x y x' y' a b c c' H H' H0))
+        | [ H : ?x - ?y + ?z <> ?w, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a - b + c <> d -> b = 0 -> a + c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x - ?y <> ?z, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a - b <> c -> b = 0 -> a <> c) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y + ?z <> ?w, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * b + c <> d -> a = 0 -> c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x * ?y + ?z <> ?w, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * b + c <> d -> b = 0 -> c <> d) ltac:(fun H'' => constr:(fun Hv => H'' x y z w Hv H'))
+        | [ H : ?x * ?y <> ?z, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b <> c -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y <> ?z, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b <> c -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : Fopp (?x * ?y) <> ?z, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, Fopp (a * b) <> c -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : Fopp (?x * ?y) <> ?z, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, Fopp (a * b) <> c -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y^3 = ?z, H' : ?y = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a * b^3 = c -> b = 0 -> c = 0)
+        | [ H : ?x * ?y = ?z, H' : ?x = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a * b = c -> a = 0 -> c = 0)
+        | [ H : ?x * ?y - ?z <> 0, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b - c <> 0 -> a = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y - ?z <> 0, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b - c <> 0 -> b = 0 -> c <> 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y - ?z = 0, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b - c = 0 -> a = 0 -> c = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * ?y - ?z = 0, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a * b - c = 0 -> b = 0 -> c = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x - ?y * ?z = 0, H' : ?z = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a - b * c = 0 -> c = 0 -> a = 0) ltac:(fun H'' => constr:(fun Hv => H'' x y z Hv H'))
+        | [ H : ?x * (?y * ?y^2) - ?z <> ?w |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c d, a * (b * b^2) - c <> d -> a * (b^3) - c <> d)
+        | [ H : ?x * (?y * ?y^2) - ?z = ?w |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c d, a * (b * b^2) - c = d -> a * (b^3) - c = d)
+        | [ H : ?x - (?y * ?y^2) * ?z <> ?w |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c d, a - (b * b^2) * c <> d -> a - (b^3) * c <> d)
+        | [ H : ?x - (?y * ?y^2) * ?z = ?w |- _ ]
+          => F.apply_lemma_in_on pkg H (forall a b c d, a - (b * b^2) * c = d -> a - (b^3) * c = d)
+        | [ H : ?x * (?y * ?y^2) = 0, H' : ?y <> 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b, a * (b * b^2) = 0 -> b <> 0 -> a = 0)
+        | [ H : ?x * (?y * ?z) = 0, H' : ?z <> 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, c <> 0 -> a * (b * c) = 0 -> a * b = 0) ltac:(fun lem => constr:(lem x y z H'))
+        | [ H : ?x = ?y * ?z, H' : ?y = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a = b * c -> b = 0 -> a = 0) ltac:(fun lem => constr:(fun H => lem x y z H H'))
+        | [ H : ?x * ?y + ?z = 0, H' : ?x = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c, a = 0 -> a * b + c = 0 -> c = 0) ltac:(fun lem => constr:(lem x y z H'))
+        | [ H : ?x * (?y * ?y^2) - ?z * ?z^2 * ?w = 0, H' : ?x * ?y^3 + ?w * ?z^3 = 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * b^3 + d * c^3 = 0 -> a * (b * b^2) - c * c^2 * d = 0 -> a * b^3 = 0) ltac:(fun lem => constr:(lem x y z w H'))
+        | [ H : ?x * Finv (?y^2) <> ?z * Finv (?w^2), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * Finv (b^2) <> c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) <> c * (b^2)) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
+        | [ H : ?x * Finv (?y^2) = ?z * Finv (?w^2), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * Finv (b^2) = c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) = c * (b^2)) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
+        | [ H : ?x * Finv (?y^3) = Fopp (?z * Finv (?w^3)), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * Finv (b^3) = Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) = Fopp (c * (b^3))) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
+        | [ H : ?x * Finv (?y^3) <> Fopp (?z * Finv (?w^3)), Hy : ?y <> 0, Hw : ?w <> 0 |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall a b c d, a * Finv (b^3) <> Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) <> Fopp (c * (b^3))) ltac:(fun Hv => constr:(fun H => Hv x y z w H Hy Hw))
+        | [ H : ?x = Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a = Fopp (b * c) -> a - c * b = 0 -> a = 0)
+        | [ H : ?x = Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a = Fopp (b * c) -> a - c * b = 0 -> a = 0)
+        | [ H : ?x <> Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a <> Fopp (b * c) -> a - c * b = 0 -> a * b * c <> 0)
+        | [ H : ?x <> Fopp (?y * ?z), H' : ?x - ?z * ?y = 0 |- _ ]
+          => F.apply2_lemma_in_on pkg H H' (forall a b c, a <> Fopp (b * c) -> a - c * b = 0 -> a * b * c <> 0)
+        | [ H : ?y^2 = ?c^3 + ?a * ?c * (?x^2)^2 + ?b * (?x^3)^2,
+                H' : ?y'^2 = ?c'^3 + ?a * ?c' * (?x'^2)^2 + ?b * (?x'^3)^2,
+                     H0 : ?c' * ?x^2 - ?c * ?x'^2 = 0
+            |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall X Y X' Y' A B C C', Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 - C * X'^2 = 0 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0) ltac:(fun Hv => constr:(fun H => Hv x y x' y' a b c c' H H' H0))
+        | [ H : ?y^2 = ?c^3 + ?a * ?c * (?x^2)^2 + ?b * (?x^3)^2,
+                H' : ?y'^2 = ?c'^3 + ?a * ?c' * (?x'^2)^2 + ?b * (?x'^3)^2,
+                     H0 : ?c' * ?x^2 = ?c * ?x'^2
+            |- _ ]
+          => F.apply_lemma_in_on' pkg H (forall X Y X' Y' A B C C', Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 = C * X'^2 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0) ltac:(fun Hv => constr:(fun H => Hv x y x' y' a b c c' H H' H0))
 
-               | [ H0 : ?n0 = 0, H1 : ?n1 = 0, H2 : ?d0 <> 0, H3 : ?d1 <> 0, H : ?n0 / ?d0^3 <> Fopp (?n1 / ?d1^3) |- _ ]
-                 => revert H0 H1 H2 H3 H; progress clear_eq_and_neq; generalize n0 n1 d0 d1; intros
-               | [ H0 : ?x * ?y^3 = ?A * ?B^3,
-                        H1 : ?x * ?z^3 - ?B^3 * ?D = 0,
-                             H2 : ?D * ?C^3 = ?w * ?z^3,
-                                  H3 : ?A * ?C^3 - ?y^3 * ?w <> 0,
-                                       Hz : ?z <> 0,
-                                            HB : ?B <> 0
-                   |- _ ]
-                 => solve [
-                        exfalso; revert H0 H1 H2 H3 Hz HB; clear_eq_and_neq;
-                        generalize x, y, z, w, A, B, C, D; intros;
-                        fsatz ]
-               | [ H0 : ?x * ?y^3 = ?A * ?B^3,
-                        H1 : ?x * ?z^3 - ?B^3 * ?D <> 0,
-                             H2 : ?D * ?C^3 = ?w * ?z^3,
-                                  H3 : ?A * ?C^3 - ?y^3 * ?w = 0,
-                                       Hy : ?y <> 0,
-                                            HC : ?C <> 0
-                   |- _ ]
-                 => solve [
-                        exfalso; revert H0 H1 H2 H3 Hy HC; clear_eq_and_neq;
-                        generalize x, y, z, w, A, B, C, D; intros;
-                        fsatz ]
-               | [ H0 : ?x * ?y^2 = ?A * ?B^2,
-                        H1 : ?x * ?z^2 - ?D * ?B^2 = 0,
-                             H2 : ?D * ?C^2 = ?w * ?z^2,
-                                  H3 : ?A * ?C^2 - ?w * ?y^2 <> 0,
-                                       Hz : ?z <> 0,
-                                            HB : ?B <> 0
-                   |- _ ]
-                 => solve [
-                        exfalso; revert H0 H1 H2 H3 Hz HB; clear_eq_and_neq;
-                        generalize x, y, z, w, A, B, C, D; intros;
-                        fsatz ]
-               | [ H0 : ?A * ?B^2 = ?x * ?y^2,
-                        H1 : ?x * ?z^2 - ?D * ?B^2 = 0,
-                             H2 : ?w * ?z^2 = ?D * ?C^2,
-                                  H3 : ?A * ?C^2 - ?w * ?y^2 <> 0,
-                                       Hz : ?z <> 0,
-                                            HB : ?B <> 0
-                   |- _ ]
-                 => solve [
-                        exfalso; revert H0 H1 H2 H3 Hz HB; clear_eq_and_neq;
-                        generalize x, y, z, w, A, B, C, D; intros;
-                        fsatz ]
-               | [ H : ?x <> 0 |- context[Finv (?x^2)] ]
-                 => find_and_do_or_prove_by_fsatz (forall a, a <> 0 -> Finv (a^2) = (Finv a)^2) ltac:(fun H' => rewrite !(H' x H))
-               | [ H : ?x <> 0 |- context[Finv (?x^3)] ]
-                 => find_and_do_or_prove_by_fsatz (forall a, a <> 0 -> Finv (a^3) = (Finv a)^3) ltac:(fun H' => rewrite !(H' x H))
-               | [ H : ?x <> 0 |- context[Finv (Finv ?x)] ]
-                 => find_and_do_or_prove_by_fsatz (forall a, a <> 0 -> Finv (Finv a) = a) ltac:(fun H' => rewrite !(H' x H))
-               | [ |- context[Finv ((?x + ?y)^2 - ?x^2 - ?y^2)] ]
-                 => find_and_do_or_prove_by_fsatz (forall a b, (a + b)^2 - a^2 - b^2 = (1+1) * a * b) ltac:(fun H' => rewrite !(H' x y))
-               | [ |- context[Finv (?x * ?y)] ]
-                 => find_and_do_or_prove_by_fsatz
-                      (forall a b, a * b <> 0 -> Finv (a * b) = Finv a * Finv b)
-                      ltac:(fun H' => rewrite !(H' x y) by (clear_eq; fsatz))
-               end.
+        | [ H0 : ?x * ?y^3 = ?A * ?B^3,
+                 H1 : ?x * ?z^3 - ?B^3 * ?D = 0,
+                      H2 : ?D * ?C^3 = ?w * ?z^3,
+                           H3 : ?A * ?C^3 - ?y^3 * ?w <> 0,
+                                Hz : ?z <> 0,
+                                     HB : ?B <> 0
+            |- _ ]
+          => exfalso; revert H0 H1 H2 H3 Hz HB;
+             generalize x, y, z, w, A, B, C, D;
+             F.goal_exact_lemma_on pkg
+        | [ H0 : ?x * ?y^3 = ?A * ?B^3,
+                 H1 : ?x * ?z^3 - ?B^3 * ?D <> 0,
+                      H2 : ?D * ?C^3 = ?w * ?z^3,
+                           H3 : ?A * ?C^3 - ?y^3 * ?w = 0,
+                                Hy : ?y <> 0,
+                                     HC : ?C <> 0
+            |- _ ]
+          => exfalso; revert H0 H1 H2 H3 Hy HC;
+             generalize x, y, z, w, A, B, C, D;
+             F.goal_exact_lemma_on pkg
+        | [ H0 : ?x * ?y^2 = ?A * ?B^2,
+                 H1 : ?x * ?z^2 - ?D * ?B^2 = 0,
+                      H2 : ?D * ?C^2 = ?w * ?z^2,
+                           H3 : ?A * ?C^2 - ?w * ?y^2 <> 0,
+                                Hz : ?z <> 0,
+                                     HB : ?B <> 0
+            |- _ ]
+          => exfalso; revert H0 H1 H2 H3 Hz HB;
+             generalize x, y, z, w, A, B, C, D;
+             F.goal_exact_lemma_on pkg
+        | [ H0 : ?A * ?B^2 = ?x * ?y^2,
+                 H1 : ?x * ?z^2 - ?D * ?B^2 = 0,
+                      H2 : ?w * ?z^2 = ?D * ?C^2,
+                           H3 : ?A * ?C^2 - ?w * ?y^2 <> 0,
+                                Hz : ?z <> 0,
+                                     HB : ?B <> 0
+            |- _ ]
+          => exfalso; revert H0 H1 H2 H3 Hz HB;
+             generalize x, y, z, w, A, B, C, D;
+             F.goal_exact_lemma_on pkg
+        | [ H : ?x <> 0 |- context[Finv (?x^2)] ]
+          => F.with_lemma_on pkg (forall a, a <> 0 -> Finv (a^2) = (Finv a)^2) ltac:(fun H' => rewrite !(H' x H))
+        | [ H : ?x <> 0 |- context[Finv (?x^3)] ]
+          => F.with_lemma_on pkg (forall a, a <> 0 -> Finv (a^3) = (Finv a)^3) ltac:(fun H' => rewrite !(H' x H))
+        | [ H : ?x <> 0 |- context[Finv (Finv ?x)] ]
+          => F.with_lemma_on pkg (forall a, a <> 0 -> Finv (Finv a) = a) ltac:(fun H' => rewrite !(H' x H))
+        | [ |- context[Finv ((?x + ?y)^2 - ?x^2 - ?y^2)] ]
+          => F.with_lemma_on pkg (forall a b, (a + b)^2 - a^2 - b^2 = (1+1) * a * b) ltac:(fun H' => rewrite !(H' x y))
+        | [ |- context[Finv ((?x + ?y)^2 - (?x^2 + ?y^2))] ]
+          => F.with_lemma_on pkg (forall a b, (a + b)^2 - (a^2 + b^2) = (1+1) * a * b) ltac:(fun H' => rewrite !(H' x y))
+        | [ |- context[Finv (?x * ?y)] ]
+          => F.with_lemma_on
+               pkg
+               (forall a b, a * b <> 0 -> Finv (a * b) = Finv a * Finv b)
+               ltac:(fun H' => rewrite !(H' x y) by (clear_eq; fsatz))
+        | _ => idtac
+        end.
+      Local Ltac speed_up_fsatz :=
+        let fld := guess_field in
+        let pkg := F.get_package_on fld in
+        divisions_to_inverses fld;
+        repeat speed_up_fsatz_step_on pkg.
+      (* sanity check to get error messages that would otherwise be gobbled by [repeat] *)
+      Local Ltac speed_up_fsatz_check :=
+        let fld := guess_field in
+        let pkg := F.get_package_on fld in
+        speed_up_fsatz_step_on pkg.
 
       (* Everything this can solve, [t] can also solve, but this does some extra work to go faster *)
+      Local Ltac pre_pre_faster_t :=
+        prept; try contradiction; speed_up_fsatz.
+      Local Ltac pre_faster_t :=
+        pre_pre_faster_t; speed_up_fsatz_check; clean_up_speed_up_fsatz.
       Local Ltac faster_t_noclear :=
-        prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz;
-        fsatz.
+        pre_faster_t; fsatz.
       Local Ltac faster_t :=
-        prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz;
+        pre_faster_t;
         try solve [ lazymatch goal with
                     | [ |- _ = _ ] => clear_neq
                     | _ => idtac
@@ -526,7 +537,7 @@ Module Jacobian.
       Lemma to_affine_add P Q
         : W.eq (to_affine (add P Q)) (W.add (to_affine P) (to_affine Q)).
       Proof.
-        Time prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz. (* 28.713 secs (17.591u,0.032s) *)
+        Time prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz. (* 15.009 secs (14.871u,0.048s) *)
         Time all: fsatz. (* 6.335 secs (6.172u,0.163s) *)
       Time Qed. (* 1.924 secs (1.928u,0.s) *)
     End AEqMinus3.
diff --git a/src/Util/FsatzAutoLemmas.v b/src/Util/FsatzAutoLemmas.v
new file mode 100644
index 000000000..b766fc411
--- /dev/null
+++ b/src/Util/FsatzAutoLemmas.v
@@ -0,0 +1,245 @@
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Morphisms.
+
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Util.Notations.
+
+Create HintDb fsatz_lookup discriminated.
+
+Module F.
+  Section with_field.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
+            {Feq_dec:DecidableRel Feq}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Infix "+" := Fadd. Local Infix "-" := Fsub.
+    Local Infix "*" := Fmul. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x).
+
+    Local Obligation Tactic := abstract (intros; fsatz).
+
+    Program Definition eq_opp__eq_zero a : a = Fopp a -> a = 0 := _.
+    Program Definition neq_opp__neq_zero a : a <> Fopp a -> a <> 0 := _.
+    Program Definition twice_eq_zero a : a + a = 0 -> a = 0 := _.
+    Program Definition twice_neq_zero a : a + a <> 0 -> a <> 0 := _.
+    Program Definition inv_cube_eq_zero__neq_zero__absurd a : Finv (a^3) = 0 -> a <> 0 -> False := _.
+    Program Definition sub_eq_zero_eq a b : a - b = 0 -> a = b := _.
+    Program Definition sub_eq_zero_eq_sym a b : a - b = 0 -> b = a := _.
+    Program Definition sub_neq_zero_eq a b : a - b <> 0 -> a <> b := _.
+    Program Definition sub_neq_zero_eq_sym a b : a - b <> 0 -> b <> a := _.
+    Program Definition mul3_nonzero_drop_mid a b c : (a * b) * c <> 0 -> a * c <> 0 := _.
+    Program Definition mul_nonzero_l a b : a * b <> 0 -> a <> 0 := _.
+    Program Definition mul_nonzero_r a b : a * b <> 0 -> b <> 0 := _.
+    Program Definition factor_difference_of_squares a b c : a^2 - b^2 = c -> (a - b) * (a + b) = c := _.
+    Program Definition expand_square_sum a b : (a + b)^2 - (a^2 + b^2) = 0 -> a * b = 0 := _.
+    Program Definition expand_square_sum_neq a b : (a + b)^2 - (a^2 + b^2) <> 0 -> a * b <> 0 := _.
+    Program Definition expand_square_sum_sub a b : (a + b)^2 - a^2 - b^2 = 0 -> a * b = 0 := _.
+    Program Definition expand_square_sum_sub_neq a b : (a + b)^2 - a^2 - b^2 <> 0 -> a * b <> 0 := _.
+    Program Definition factor_square_sum a b : a * b = 0 -> (a + b)^2 - (a^2 + b^2) = 0 := _.
+    Program Definition factor_square_sum_neq a b : a * b <> 0 -> (a + b)^2 - (a^2 + b^2) <> 0 := _.
+    Program Definition factor_square_sum_sub a b : a * b = 0 -> (a + b)^2 - a^2 - b^2 = 0 := _.
+    Program Definition factor_square_sum_sub_neq a b : a * b <> 0 -> (a + b)^2 - a^2 - b^2 <> 0 := _.
+    Program Definition mul_eq_0_r_nz a b : a * b = 0 -> a <> 0 -> b = 0 := _.
+    Program Definition mul_eq_0_l_nz a b : a * b = 0 -> b <> 0 -> a = 0 := _.
+    Program Definition mul_eq_0_l a b : a = 0 -> a * b = 0 := _.
+    Program Definition mul_eq_0_r a b : b = 0 -> a * b = 0 := _.
+    Program Definition mul_neq_0 a b : a <> 0 -> b <> 0 -> a * b <> 0 := _.
+    Program Definition helper1 a b c : a + b * c = 0 -> a <> Fopp (c * b) -> False := _.
+    Program Definition helper2 a b c d : a - b * c <> d -> b = 1 -> a - c <> d := _.
+    Program Definition helper3 a b c d : a - b * c = d -> b = 1 -> a - c = d := _.
+    Program Definition helper4 a b c d e : a - b * c * d <> e -> b = 1 -> a - c * d <> e := _.
+    Program Definition helper5 a b c d e : a - b * c * d = e -> b = 1 -> a - c * d = e := _.
+    Program Definition helper6 a b c d : a - b * c^2 <> d -> c = 1 -> a - b <> d := _.
+    Program Definition helper7 a b c d : a - b * c^2 = d -> c = 1 -> a - b = d := _.
+    Program Definition helper8 a b c d : a - b + c <> d -> b = 0 -> a + c <> d := _.
+    Program Definition helper9 a b c : a - b <> c -> b = 0 -> a <> c := _.
+    Program Definition helper10 a b c d : a * b + c <> d -> a = 0 -> c <> d := _.
+    Program Definition helper11 a b c d : a * b + c <> d -> b = 0 -> c <> d := _.
+    Program Definition helper12 a b c : a * b <> c -> a = 0 -> c <> 0 := _.
+    Program Definition helper13 a b c : a * b <> c -> b = 0 -> c <> 0 := _.
+    Program Definition helper14 a b c : Fopp (a * b) <> c -> a = 0 -> c <> 0 := _.
+    Program Definition helper15 a b c : Fopp (a * b) <> c -> b = 0 -> c <> 0 := _.
+    Program Definition helper16 a b c : a * b^3 = c -> b = 0 -> c = 0 := _.
+    Program Definition helper17 a b c : a * b = c -> a = 0 -> c = 0 := _.
+    Program Definition helper18 a b c : a * b - c <> 0 -> a = 0 -> c <> 0 := _.
+    Program Definition helper19 a b c : a * b - c <> 0 -> b = 0 -> c <> 0 := _.
+    Program Definition helper20 a b c : a * b - c = 0 -> a = 0 -> c = 0 := _.
+    Program Definition helper21 a b c : a * b - c = 0 -> b = 0 -> c = 0 := _.
+    Program Definition helper22 a b c : a - b * c = 0 -> c = 0 -> a = 0 := _.
+    Program Definition helper23 a b c d : a * (b * b^2) - c <> d -> a * (b^3) - c <> d := _.
+    Program Definition helper24 a b c d : a * (b * b^2) - c = d -> a * (b^3) - c = d := _.
+    Program Definition helper25 a b c d : a - (b * b^2) * c <> d -> a - (b^3) * c <> d := _.
+    Program Definition helper26 a b c d : a - (b * b^2) * c = d -> a - (b^3) * c = d := _.
+    Program Definition helper27 a b : a * (b * b^2) = 0 -> b <> 0 -> a = 0 := _.
+    Program Definition helper28 a b c : c <> 0 -> a * (b * c) = 0 -> a * b = 0 := _.
+    Program Definition helper29 a b c : a = 0 -> a * b + c = 0 -> c = 0 := _.
+    Program Definition helper30 a b c d : a * b^3 + d * c^3 = 0 -> a * (b * b^2) - c * c^2 * d = 0 -> a * b^3 = 0 := _.
+    Program Definition helper31 a b c d : a * Finv (b^2) <> c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) <> c * (b^2) := _.
+    Program Definition helper32 a b c d : a * Finv (b^2) = c * Finv (d^2) -> b <> 0 -> d <> 0 -> a * (d^2) = c * (b^2) := _.
+    Program Definition helper33 a b c d : a * Finv (b^3) = Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) = Fopp (c * (b^3)) := _.
+    Program Definition helper34 a b c d : a * Finv (b^3) <> Fopp (c * Finv (d^3)) -> b <> 0 -> d <> 0 -> a * (d^3) <> Fopp (c * (b^3)) := _.
+    Program Definition helper35 a b c : a = Fopp (b * c) -> a - c * b = 0 -> a = 0 := _.
+    Program Definition helper36 a b c : a <> Fopp (b * c) -> a - c * b = 0 -> a * b * c <> 0 := _.
+    Program Definition helper37 X Y X' Y' A B C C' : Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 - C * X'^2 = 0 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0 := _.
+    Program Definition helper38 X Y X' Y' A B C C' : Y^2 = C^3 + A * C * (X^2)^2 + B * (X^3)^2 -> Y'^2 = C'^3 + A * C' * (X'^2)^2 + B * (X'^3)^2 -> C' * X^2 = C * X'^2 -> (Y' * (X^3))^2 - ((X'^3) * Y)^2 = 0 := _.
+    Program Definition helper39 a : a <> 0 -> Finv (a^2) = (Finv a)^2 := _.
+    Program Definition helper40 a : a <> 0 -> Finv (a^3) = (Finv a)^3 := _.
+    Program Definition helper41 a : a <> 0 -> Finv (Finv a) = a := _.
+    Program Definition helper42 a b : (a + b)^2 - a^2 - b^2 = (1+1) * a * b := _.
+    Program Definition helper42' a b : (a + b)^2 - (a^2 + b^2) = (1+1) * a * b := _.
+    Program Definition helper43 a b : a * b <> 0 -> Finv (a * b) = Finv a * Finv b := _.
+    Program Definition helper_zero_1 a b c : a = b * c -> b = 0 -> a = 0 := _.
+    Program Definition helper44 x y z w A B C D
+            (H0 : x * y^3 = A * B^3)
+            (H1 : x * z^3 - B^3 * D = 0)
+            (H2 : D * C^3 = w * z^3)
+            (H3 : A * C^3 - y^3 * w <> 0)
+            (Hz : z <> 0)
+            (HB : B <> 0)
+            : False := _.
+    Program Definition helper45 x y z w A B C D
+            (H0 : x * y^3 = A * B^3)
+            (H1 : x * z^3 - B^3 * D <> 0)
+            (H2 : D * C^3 = w * z^3)
+            (H3 : A * C^3 - y^3 * w = 0)
+            (Hy : y <> 0)
+            (HC : C <> 0)
+      : False := _.
+    Program Definition helper46 x y z w A B C D
+            (H0 : x * y^2 = A * B^2)
+            (H1 : x * z^2 - D * B^2 = 0)
+            (H2 : D * C^2 = w * z^2)
+            (H3 : A * C^2 - w * y^2 <> 0)
+            (Hz : z <> 0)
+            (HB : B <> 0)
+      : False := _.
+    Program Definition helper47 x y z w A B C D
+            (H0 : A * B^2 = x * y^2)
+            (H1 : x * z^2 - D * B^2 = 0)
+            (H2 : w * z^2 = D * C^2)
+            (H3 : A * C^2 - w * y^2 <> 0)
+            (Hz : z <> 0)
+            (HB : B <> 0)
+      : False := _.
+
+    Record dyn := { ty : Prop ; lem : ty }.
+
+    Local Notation "[ x , .. , z ]"
+      := (cons {| lem := x |} .. (cons {| lem := z |} nil) .. ).
+
+    (* grep -o 'Program Definition [^ ]*' src/Util/FsatzAutoLemmas.v  | sed s'/Program Definition /, /g' *)
+    Definition all_lemmas
+      := [I
+          , eq_opp__eq_zero
+          , neq_opp__neq_zero
+          , twice_eq_zero
+          , twice_neq_zero
+          , inv_cube_eq_zero__neq_zero__absurd
+          , sub_eq_zero_eq
+          , sub_eq_zero_eq_sym
+          , sub_neq_zero_eq
+          , sub_neq_zero_eq_sym
+          , mul3_nonzero_drop_mid
+          , mul_nonzero_l
+          , mul_nonzero_r
+          , factor_difference_of_squares
+          , expand_square_sum
+          , expand_square_sum_neq
+          , expand_square_sum_sub
+          , expand_square_sum_sub_neq
+          , factor_square_sum
+          , factor_square_sum_neq
+          , factor_square_sum_sub
+          , factor_square_sum_sub_neq
+          , mul_eq_0_r_nz
+          , mul_eq_0_l_nz
+          , mul_eq_0_l
+          , mul_eq_0_r
+          , mul_neq_0
+          , helper1
+          , helper2
+          , helper3
+          , helper4
+          , helper5
+          , helper6
+          , helper7
+          , helper8
+          , helper9
+          , helper10
+          , helper11
+          , helper12
+          , helper13
+          , helper14
+          , helper15
+          , helper16
+          , helper17
+          , helper18
+          , helper19
+          , helper20
+          , helper21
+          , helper22
+          , helper23
+          , helper24
+          , helper25
+          , helper26
+          , helper27
+          , helper28
+          , helper29
+          , helper30
+          , helper31
+          , helper32
+          , helper33
+          , helper34
+          , helper35
+          , helper36
+          , helper37
+          , helper38
+          , helper39
+          , helper40
+          , helper41
+          , helper42
+          , helper42'
+          , helper43
+          , helper_zero_1
+          , helper44
+          , helper45
+          , helper46
+          , helper47
+         ].
+  End with_field.
+
+  Ltac get_package_on fld :=
+    let pkg := constr:(all_lemmas (field:=fld)) in
+    let pkg := (eval cbv [all_lemmas] in pkg) in
+    pkg.
+
+  Ltac lookup_lemma_on pkg ty :=
+    lazymatch pkg with
+    | context[@Build_dyn ty ?lem] => lem
+    end.
+
+  Ltac lookup_lemma ty :=
+    let fld := guess_field in
+    let pkg := get_package_on fld in
+    lookup_lemma_on fld ty.
+
+  Ltac with_lemma_on pkg ty tac :=
+    let H := lookup_lemma_on pkg ty in
+    tac H.
+
+  Ltac goal_exact_lemma_on pkg :=
+    lazymatch goal with
+    | [ |- ?G ] => with_lemma_on pkg G ltac:(fun H' => exact H')
+    end.
+  Ltac goal_apply_lemma_on pkg ty :=
+    with_lemma_on pkg ty ltac:(fun H' => apply H').
+  Ltac apply_lemma_in_on pkg H ty :=
+    with_lemma_on pkg ty ltac:(fun H' => apply H' in H).
+  Ltac apply2_lemma_in_on pkg H0 H1 ty :=
+    with_lemma_on pkg ty ltac:(fun H' => apply H' in H0; [ | exact H1 ]).
+  Ltac apply_lemma_in_on' pkg H ty preapp :=
+    with_lemma_on pkg ty ltac:(fun H' => let H' := preapp H' in apply H' in H).
+End F.