Massively speed up Jacobian

After    | File Name                   | Before    || Change     | % Change
---------------------------------------------------------------------------
1m52.31s | Total                       | 13m36.75s || -11m44.44s | -86.24%
---------------------------------------------------------------------------
1m52.31s | Curves/Weierstrass/Jacobian | 13m36.75s || -11m44.44s | -86.24%

1 files changed, 342 insertions, 25 deletions

diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v
index 323816b81..d16696823 100644
--- a/src/Curves/Weierstrass/Jacobian.v
+++ b/src/Curves/Weierstrass/Jacobian.v
@@ -33,24 +33,35 @@ Module Jacobian.
              /\ Y1*Z2^3 = Y2*Z1^3
       end.
 
-    Ltac prept :=
-      repeat match goal with
-             | _ => progress intros
-             | _ => progress specialize_by trivial
-             | _ => progress cbv [proj1_sig fst snd]
-             | _ => progress autounfold with points_as_coordinates in *
-             | _ => progress destruct_head'_True
-             | _ => progress destruct_head'_unit
-             | _ => progress destruct_head'_prod
-             | _ => progress destruct_head'_sig
-             | _ => progress destruct_head'_and
-             | _ => progress destruct_head'_sum
-             | _ => progress destruct_head'_bool
-             | _ => progress destruct_head'_or
-             | H: context[dec ?P] |- _ => destruct (dec P)
-             | |- context[dec ?P]      => destruct (dec P)
-             | |- ?P => lazymatch type of P with Prop => split end
-             end.
+    (* These cases are not needed to solve the goal, but handling them early speeds things up considerably *)
+    Ltac prept_step_opt :=
+      match goal with
+      | [ H : ?T |- ?T ] => exact H
+      | [ |- ?x = ?x ] => reflexivity
+      | [ H : ?T, H' : ~?T |- _ ] => solve [ exfalso; apply H', H ]
+      end.
+
+    Ltac prept_step :=
+      match goal with
+      | _ => progress prept_step_opt
+      | _ => progress intros
+      (*| _ => progress specialize_by_assumption*)
+      (*| _ => progress specialize_by trivial*)
+      | _ => progress cbv [proj1_sig fst snd] in *
+      | _ => progress autounfold with points_as_coordinates in *
+      | _ => progress destruct_head'_True
+      | _ => progress destruct_head'_unit
+      | _ => progress destruct_head'_prod
+      | _ => progress destruct_head'_sig
+      | _ => progress destruct_head'_and
+      | _ => progress destruct_head'_sum
+      | _ => progress destruct_head'_bool
+      | _ => progress destruct_head'_or
+      | H: context[@dec ?P ?pf] |- _ => destruct (@dec P pf)
+      | |- context[@dec ?P ?pf]      => destruct (@dec P pf)
+      | |- ?P => lazymatch type of P with Prop => split end
+      end.
+    Ltac prept := repeat prept_step.
     Ltac t := prept; trivial; try contradiction; fsatz.
 
     Create HintDb points_as_coordinates discriminated.
@@ -131,6 +142,309 @@ Module Jacobian.
         | true => z_is_zero_or_one Q
         end.
 
+      Local Ltac clear_neq :=
+        repeat match goal with
+               | [ H : _ <> _ |- _ ] => clear H
+               end.
+      Local Ltac clear_eq :=
+        repeat match goal with
+               | [ H : _ = _ |- _ ] => clear H
+               end.
+      Local Ltac clear_eq_and_neq :=
+        repeat (clear_eq || clear_neq).
+      Local Ltac clean_up_speed_up_fsatz :=
+        repeat match goal with
+               | [ H : forall a : F, _ = _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a : F, _ <> _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a : F, _ <> _ -> _ <> _ |- _ ] => clear H
+               | [ H : forall a b : F, _ = _ |- _ ] => clear H
+               | [ H : forall a b : F, _ = _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a b : F, _ <> _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a b : F, _ <> _ -> _ <> _ |- _ ] => clear H
+               | [ H : forall a b : F, _ = _ -> _ <> _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a b : F, _ <> _ -> _ <> _ -> _ = _ |- _ ] => clear H
+               | [ H : forall a b : F, _ <> _ -> _ <> _ -> _ <> _ |- _ ] => clear H
+               | [ H : forall a b c : F, _ |- _ ] => clear H
+               | [ H : ?T, H' : ?T |- _ ] => clear H'
+               | [ H : ?x = ?x |- _ ] => clear H
+               | [ H : ?x <> 0, H' : ?x = 1 |- _ ] => clear H
+               | [ H : ?x = 0 |- _ ] => is_var x; clear H x
+               | [ H : ?x = 1 |- _ ] => is_var x; clear H x
+               | [ H : Finv (?x^3) <> 0, H' : ?x <> 0 |- _ ] => clear H
+               end.
+      Local Ltac find_and_do_or_prove_by ty by_tac tac :=
+        lazymatch goal with
+        | [ H' : ty |- _ ]
+          => tac H'
+        | _
+          => assert ty by by_tac
+        end.
+      Local Ltac find_and_do_or_prove_by_fsatz ty tac :=
+        find_and_do_or_prove_by ty ltac:(clear_eq_and_neq; intros; fsatz) tac.
+      Local Ltac find_and_do_or_prove_by_fsatz_with_neq ty tac :=
+        find_and_do_or_prove_by ty ltac:(clear_neq; intros; fsatz) tac.
+      Local Ltac find_and_goal_apply_or_prove_by_fsatz ty :=
+        find_and_do_or_prove_by_fsatz ty ltac:(fun H' => apply H').
+      Local Ltac find_and_apply_or_prove_by_fsatz H ty :=
+        find_and_do_or_prove_by_fsatz ty ltac:(fun H' => apply H' in H).
+      Local Ltac find_and_apply_or_prove_by_fsatz2 H0 H1 ty :=
+        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)
+
+               | [ 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 = 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))
+
+               | [ 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.
+
+      (* Everything this can solve, [t] can also solve, but this does some extra work to go faster *)
+      Local Ltac faster_t_noclear :=
+        prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz;
+        fsatz.
+      Local Ltac faster_t :=
+        prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz;
+        try solve [ lazymatch goal with
+                    | [ |- _ = _ ] => clear_neq
+                    | _ => idtac
+                    end;
+                    fsatz ].
+
       Hint Unfold double negb andb add_precondition z_is_zero_or_one : points_as_coordinates.
       Program Definition add_impl (mixed : bool) (P Q : point)
               (H : add_precondition Q mixed) : point :=
@@ -189,7 +503,8 @@ Module Jacobian.
             let z3 := if z2nz then z_out else z1 in
             (x3, y3, z3)
         end.
-      Next Obligation. Proof. t. Qed.
+      Next Obligation. Proof. faster_t_noclear. Qed.
+
       Definition add (P Q : point) : point :=
         add_impl false P Q I.
       Definition add_mixed (P : point) (Q : point) (H : z_is_zero_or_one Q) :=
@@ -197,23 +512,25 @@ Module Jacobian.
 
       Hint Unfold W.eq W.add to_affine add add_mixed add_impl : points_as_coordinates.
 
-      Lemma Proper_double : Proper (eq ==> eq) double. Proof. t. Qed.
+      Lemma Proper_double : Proper (eq ==> eq) double. Proof. faster_t_noclear. Qed.
       Lemma to_affine_double P :
         W.eq (to_affine (double P)) (W.add (to_affine P) (to_affine P)).
-      Proof. t. Qed.
+      Proof. faster_t_noclear. Qed.
 
       Lemma add_mixed_eq_add (P : point) (Q : point) (H : z_is_zero_or_one Q) :
         eq (add P Q) (add_mixed P Q H).
-      Proof. t. Qed.
+      Proof. faster_t. Qed.
 
-      Lemma Proper_add : Proper (eq ==> eq ==> eq) add. Proof. t. Qed.
+      Lemma Proper_add : Proper (eq ==> eq ==> eq) add. Proof. faster_t_noclear. Qed.
       Import BinPos.
       Lemma to_affine_add
             {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12} (* TODO: why do we need 12 instead of 3? *)
             P Q
         : W.eq (to_affine (add P Q)) (W.add (to_affine P) (to_affine Q)).
-      Proof. prept; trivial; try contradiction. Time all: abstract t. Time Qed.
-      (* 306.478 secs (43.916u,1.032s) ;; 18.857 secs (18.856u,0.008s) *)
+      Proof.
+        Time prept; try contradiction; speed_up_fsatz; clean_up_speed_up_fsatz. (* 28.713 secs (17.591u,0.032s) *)
+        Time all: fsatz. (* 6.335 secs (6.172u,0.163s) *)
+      Time Qed. (* 1.924 secs (1.928u,0.s) *)
     End AEqMinus3.
   End Jacobian.
 End Jacobian.