Generalize Jacobian.v over all a.

The immediate motivation is BoringSSL's generic EC code is sadly stuck
with supporting arbitrary curves, including those where a <> -3, but it
may be more generally useful.

This makes the file slightly more general:

- It now proves that the addition formula works independent of a = -3.

- It proves a generic doubling implementation, based on
  http://www.hyperelliptic.org/EFD/g1p/auto-shortw-jacobian.html#doubling-dbl-2007-bl

- There's a place to stick in other specializations should someone want
  them. (I hear some folks are interested in secp256k1 for some reason.)

1 files changed, 454 insertions, 407 deletions

diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v
index a44ac7159..fd3b128b6 100644
--- a/src/Curves/Weierstrass/Jacobian.v
+++ b/src/Curves/Weierstrass/Jacobian.v
@@ -99,10 +99,460 @@ Module Jacobian.
       end.
     Next Obligation. Proof. t. Qed.
 
+    (** See http://www.hyperelliptic.org/EFD/g1p/auto-shortw-jacobian.html#doubling-dbl-2007-bl *)
+    Program Definition double (P : point) : point :=
+      match proj1_sig P return F*F*F with
+      | (x_in, y_in, z_in) =>
+        let xx := x_in^2 in
+        let yy := y_in^2 in
+        let yyyy := yy^2 in
+        let zz := z_in^2 in
+        (** [s = 2*((x_in + yy)^2 - xx - yyyy)] *)
+        let s := x_in + yy in
+        let s := s^2 in
+        let s := s - xx in
+        let s := s - yyyy in
+        let s := s + s in
+        (** [m = 3*xx + a*zz^2] *)
+        let m := zz^2 in
+        let m := a * m in
+        let m := m + xx in
+        let m := m + xx in
+        let m := m + xx in
+        (** [x_out = m^2 - 2*s] *)
+        let x_out := m^2 in
+        let x_out := x_out - s in
+        let x_out := x_out - s in
+        (** [z_out = (y_in + z_in)^2 - yy - zz] *)
+        let z_out := y_in + z_in in
+        let z_out := z_out^2 in
+        let z_out := z_out - yy in
+        let z_out := z_out - zz in
+        (** [y_out = m*(s-x_out) - 8*yyyy] *)
+        let yyyy := yyyy + yyyy in
+        let yyyy := yyyy + yyyy in
+        let yyyy := yyyy + yyyy in
+        let y_out := s - x_out in
+        let y_out := y_out * m in
+        let y_out := y_out - yyyy in
+        (x_out, y_out, z_out)
+      end.
+    Next Obligation. Proof. t. Qed.
+
+    Definition z_is_zero_or_one (Q : point) : Prop :=
+      match proj1_sig Q with
+      | (_, _, z) => z = 0 \/ z = 1
+      end.
+
+    Definition add_precondition (Q : point) (mixed : bool) : Prop :=
+      match mixed with
+      | false => True
+      | 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_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 |- _ ]
+        => 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 |- _ ]
+        => 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 : ?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 :=
+      pre_faster_t; fsatz.
+    Local Ltac faster_t :=
+      pre_faster_t;
+      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 :=
+      match proj1_sig P, proj1_sig Q return F*F*F with
+      | (x1, y1, z1), (x2, y2, z2) =>
+        let z1nz := if dec (z1 = 0) then false else true in
+        let z2nz := if dec (z2 = 0) then false else true in
+        let z1z1 := z1^2 in
+        let '(u1, s1, two_z1z2) := if negb mixed
+                                   then
+                                     let z2z2 := z2^2 in
+                                     let u1 := x1 * z2z2 in
+                                     let two_z1z2 := z1 + z2 in
+                                     let two_z1z2 := two_z1z2^2 in
+                                     let two_z1z2 := two_z1z2 - z1z1 in
+                                     let two_z1z2 := two_z1z2 - z2z2 in
+                                     let s1 := z2 * z2z2 in
+                                     let s1 := s1 * y1 in
+                                     (u1, s1, two_z1z2)
+                                   else
+                                     let u1 := x1 in
+                                     let two_z1z2 := z1 + z1 in
+                                     let s1 := y1 in
+                                     (u1, s1, two_z1z2)
+        in
+        let u2 := x2 * z1z1 in
+        let h := u2 - u1 in
+        let xneq := if dec (h = 0) then false else true in
+        let z_out := h * two_z1z2 in
+        let z1z1z1 := z1 * z1z1 in
+        let s2 := y2 * z1z1z1 in
+        let r := s2 - s1 in
+        let r := r + r in
+        let yneq := if dec (r = 0) then false else true in
+        if (negb xneq && negb yneq && z1nz && z2nz)%bool
+        then proj1_sig (double P)
+        else
+          let i := h + h in
+          let i := i^2 in
+          let j := h * i in
+          let v := u1 * i in
+          let x_out := r^2 in
+          let x_out := x_out - j in
+          let x_out := x_out - v in
+          let x_out := x_out - v in
+          let y_out := v - x_out in
+          let y_out := y_out * r in
+          let s1j := s1 * j in
+          let y_out := y_out - s1j in
+          let y_out := y_out - s1j in
+          let x_out := if z1nz then x_out else x2 in
+          let x3 := if z2nz then x_out else x1 in
+          let y_out := if z1nz then y_out else y2 in
+          let y3 := if z2nz then y_out else y1 in
+          let z_out := if z1nz then z_out else z2 in
+          let z3 := if z2nz then z_out else z1 in
+          (x3, y3, z3)
+      end.
+    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) :=
+      add_impl true P Q H.
+
+    Hint Unfold W.eq W.add to_affine add add_mixed add_impl : points_as_coordinates.
+
+    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. 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. faster_t. Qed.
+
+    Lemma Proper_add : Proper (eq ==> eq ==> eq) add. Proof. faster_t_noclear. Qed.
+    Import BinPos.
+    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. (* 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) *)
+
+    (** If [a] is -3, one can substitute a faster implementation of [double]. *)
     Section AEqMinus3.
       Context (a_eq_minus3 : a = Fopp (1+1+1)).
 
-      Program Definition double (P : point) : point :=
+      Program Definition double_minus_3 (P : point) : point :=
         match proj1_sig P return F*F*F with
         | (x_in, y_in, z_in) =>
           let delta := z_in^2 in
@@ -132,414 +582,11 @@ Module Jacobian.
         end.
       Next Obligation. Proof. t. Qed.
 
-      Definition z_is_zero_or_one (Q : point) : Prop :=
-        match proj1_sig Q with
-        | (_, _, z) => z = 0 \/ z = 1
-        end.
-
-      Definition add_precondition (Q : point) (mixed : bool) : Prop :=
-        match mixed with
-        | false => True
-        | 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_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 |- _ ]
-          => 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 |- _ ]
-          => 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))
+      Hint Unfold double_minus_3 : points_as_coordinates.
 
-        | [ 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 :=
-        pre_faster_t; fsatz.
-      Local Ltac faster_t :=
-        pre_faster_t;
-        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 :=
-        match proj1_sig P, proj1_sig Q return F*F*F with
-        | (x1, y1, z1), (x2, y2, z2) =>
-          let z1nz := if dec (z1 = 0) then false else true in
-          let z2nz := if dec (z2 = 0) then false else true in
-          let z1z1 := z1^2 in
-          let '(u1, s1, two_z1z2) := if negb mixed
-          then
-            let z2z2 := z2^2 in
-            let u1 := x1 * z2z2 in
-            let two_z1z2 := z1 + z2 in
-            let two_z1z2 := two_z1z2^2 in
-            let two_z1z2 := two_z1z2 - z1z1 in
-            let two_z1z2 := two_z1z2 - z2z2 in
-            let s1 := z2 * z2z2 in
-            let s1 := s1 * y1 in
-            (u1, s1, two_z1z2)
-          else
-            let u1 := x1 in
-            let two_z1z2 := z1 + z1 in
-            let s1 := y1 in
-            (u1, s1, two_z1z2)
-          in
-          let u2 := x2 * z1z1 in
-          let h := u2 - u1 in
-          let xneq := if dec (h = 0) then false else true in
-          let z_out := h * two_z1z2 in
-          let z1z1z1 := z1 * z1z1 in
-          let s2 := y2 * z1z1z1 in
-          let r := s2 - s1 in
-          let r := r + r in
-          let yneq := if dec (r = 0) then false else true in
-          if (negb xneq && negb yneq && z1nz && z2nz)%bool
-          then proj1_sig (double P)
-          else
-            let i := h + h in
-            let i := i^2 in
-            let j := h * i in
-            let v := u1 * i in
-            let x_out := r^2 in
-            let x_out := x_out - j in
-            let x_out := x_out - v in
-            let x_out := x_out - v in
-            let y_out := v - x_out in
-            let y_out := y_out * r in
-            let s1j := s1 * j in
-            let y_out := y_out - s1j in
-            let y_out := y_out - s1j in
-            let x_out := if z1nz then x_out else x2 in
-            let x3 := if z2nz then x_out else x1 in
-            let y_out := if z1nz then y_out else y2 in
-            let y3 := if z2nz then y_out else y1 in
-            let z_out := if z1nz then z_out else z2 in
-            let z3 := if z2nz then z_out else z1 in
-            (x3, y3, z3)
-        end.
-      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) :=
-        add_impl true P Q H.
-
-      Hint Unfold W.eq W.add to_affine add add_mixed add_impl : points_as_coordinates.
-
-      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. 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).
+      Lemma double_minus_3_eq_double (P : point) :
+        eq (double P) (double_minus_3 P).
       Proof. faster_t. Qed.
-
-      Lemma Proper_add : Proper (eq ==> eq ==> eq) add. Proof. faster_t_noclear. Qed.
-      Import BinPos.
-      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. (* 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.
   End Jacobian.
 End Jacobian.