Merge branch 'master' of github.mit.edu:plv/fiat-crypto

9 files changed, 362 insertions, 272 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index 8bb2148db..4162d4c1c 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -1,5 +1,6 @@
 Require Import Zpower ZArith Znumtheory.
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
+Require Import Crypto.Galois.ZGaloisField.
 Require Import Crypto.Curves.PointFormats.
 
 Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *)
@@ -9,7 +10,11 @@ Module Modulus25519 <: Modulus.
 End Modulus25519.
 
 Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
-  Module Import GFDefs := GaloisDefs Modulus25519.
+  Module Import GFDefs := ZGaloisField Modulus25519.
+
+  Lemma char_gt_2 : inject 2 <> 0%GF.
+  Admitted.
+
   Local Open Scope GF_scope.
   Coercion inject : Z >-> GF.
 
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 1e8df9337..32e6acdd0 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,18 +1,15 @@
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField.
 Require Import Tactics.VerdiTactics.
 Require Import Logic.Eqdep_dec.
 Require Import BinNums NArith.
 
-Module GaloisDefs (M : Modulus).
-  Module Export GT := GaloisTheory M.
-End GaloisDefs.
-
 Module Type TwistedEdwardsParams (M : Modulus).
-  Module Export GFDefs := GaloisDefs M.
+  Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
+  Axiom char_gt_2 : inject 2 <> 0.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
-  Axiom a_square : exists x, x * x = a.
+  Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End TwistedEdwardsParams.
@@ -116,6 +113,129 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Definition point := { P | onCurve P}.
   Definition mkPoint := exist onCurve.
 
+  Lemma GFdecidable_neq : forall x y : GF, Zbool.Zeq_bool x y = false -> x <> y.
+  Proof.
+    intros. intro. rewrite GFcomplete in H; intuition.
+  Qed.
+
+  Ltac case_eq_GF a b :=
+    case_eq (Zbool.Zeq_bool a b); intro Hx;
+    match type of Hx with
+    | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = true =>
+        pose proof (GFdecidable a b Hx)
+    | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = false =>
+        pose proof (GFdecidable_neq a b Hx)
+    end; clear Hx.
+
+  Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
+  Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
+
+  (* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *)
+  (* c=1 and an extra a in front of x^2 *) 
+
+  Lemma root_zero : forall x p, x^p = 0 -> x = 0.
+  Admitted.
+  Lemma root_nonzero : forall x p, x^p <> 0 -> x <> 0.
+  Admitted.
+  Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
+  Admitted.
+  Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
+  Admitted.
+  Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+  Admitted.
+  Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+  Admitted.
+  Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
+  Admitted.
+  Hint Resolve mul_nonzero_nonzero.
+
+  Ltac whatsNotZero :=
+    repeat match goal with
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (lhs <> 0) by (rewrite H; auto)
+    | [H: ?lhs = ?rhs |- _ ] =>
+        match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (rhs <> 0) by (rewrite H; auto)
+    | [H: (?a^?p)%GF <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (a <> 0) by (eapply root_nonzero; eauto)
+    | [H: (?a*?b)%GF <> 0 |- _ ] =>
+        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (a <> 0) by (eapply mul_nonzero_l; eauto)
+    | [H: (?a*?b)%GF <> 0 |- _ ] =>
+        match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
+        assert (b <> 0) by (eapply mul_nonzero_r; eauto)
+    end.
+
+  Lemma edwardsAddComplete' x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (d*x1*x2*y1*y2)^2 <> 1.
+  Proof.
+    unfold onCurve; intuition; whatsNotZero.
+
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+    destruct a_square as [sqrt_a a_square].
+    rewrite <- a_square in *.
+
+    (* Furthermore... *)
+    pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
+    rewrite H0 in Heqt at 2.
+    replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2))
+       with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field.
+    rewrite H1 in Heqt.
+    replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
+    rewrite <-H in Heqt.
+
+    (* main equation for both potentially nonzero denominators *)
+    case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0;
+      try match goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
+        assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 =
+                 f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2)
+                   (d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1)) as Heqw1 by field;
+        rewrite H1 in *;
+        replace (1 * y1^2) with (y1^2) in * by field;
+        rewrite <- Heqt in *;
+        assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 /
+                                 (x1 * y1 * (f (sqrt_a * x2)  y2))^2)
+                                 by (rewriteAny; field; auto);
+        match goal with [H: d = (?n^2)/(?l^2) |- _ ] =>
+            destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
+        end
+      end.
+
+    assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
+    replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field.
+
+    (* contradiction: product of nonzero things is zero *)
+    destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition];
+    destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero; field.
+  Qed.
+  
+  Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (1 + d*x1*x2*y1*y2) <> 0.
+  Proof.
+    unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF.
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field.
+      intro; rewrite H2 in H1; intuition.
+  Qed.
+  
+  Lemma edwardsAddCompletePlusMinus x1 y1 x2 y2 :
+    onCurve (x1,y1) ->
+    onCurve (x2, y2) ->
+    (1 - d*x1*x2*y1*y2) <> 0.
+  Proof.
+    unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF.
+    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
+    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field.
+      intro; rewrite H2 in H1; apply H1; field.
+  Qed.
+  Hint Resolve edwardsAddCompletePlus edwardsAddCompletePlusMinus.
+
   Definition projX (P:point) := fst (proj1_sig P).
   Definition projY (P:point) := snd (proj1_sig P).
 
@@ -125,7 +245,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   Hint Unfold onCurve mkPoint.
 
   Definition zero : point. exists (0, 1).
-    abstract (unfold onCurve; ring).
+    abstract (unfold onCurve; field).
   Defined.
 
   Definition unifiedAdd' (P1' P2' : (GF*GF)) :=
@@ -133,14 +253,55 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
     let '(x2, y2) := P2' in
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
 
-  Definition unifiedAdd (P1 P2 : point) : point. refine (
+  Lemma unifiedAdd'_onCurve x1 y1 x2 y2 x3 y3
+    (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
+    onCurve (x1,y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
+  Proof.
+    (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
+      * c=1 and an extra a in front of x^2 *) 
+    unfold unifiedAdd', onCurve in *; injection H; clear H; intros.
+
+    Ltac t x1 y1 x2 y2 :=
+      assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
+             = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
+      assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
+             = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
+    t x1 y1 x2 y2; t x2 y2 x1 y1.
+
+    remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
+      (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
+    assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
+    assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
+    (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
+     y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
+    replace 1 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
+
+    match goal with [ |- ?x = 1 ] => replace x with
+    ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
+     ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
+      d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
+    ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto.
+    - rewrite <-HT1, <-HT2; field; rewrite HT1;
+      replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
+         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
+           by field; simpl; auto.
+    - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
+         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
+           by field; auto.
+  Qed.
+
+  Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 ->
+    onCurve (unifiedAdd' P1 P2).
+  Proof.
+    intros; destruct P1, P2.
+    remember (unifiedAdd' (g, g0) (g1, g2)) as p; destruct p.
+    eapply unifiedAdd'_onCurve; eauto.
+  Qed.
+
+  Definition unifiedAdd (P1 P2 : point) : point :=
     let 'exist P1' pf1 := P1 in
     let 'exist P2' pf2 := P2 in
-    mkPoint (unifiedAdd' P1' P2') _).
-  Proof.
-    destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve.
-    admit. (* field will likely work here, but I have not done this by hand *)
-  Defined.
+    mkPoint (unifiedAdd' P1' P2') (unifiedAdd'_onCurve' _ _ pf1 pf2).
   Local Infix "+" := unifiedAdd.
 
   Fixpoint scalarMult (n:nat) (P : point) : point :=
@@ -179,18 +340,6 @@ End CompleteTwistedEdwardsPointFormat.
 Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M).
   Local Open Scope GF_scope.
   Module Import Curve := CompleteTwistedEdwardsCurve M P.
-  Lemma twistedAddCompletePlus : forall (P1 P2:point),
-    let '(x1, y1) := proj1_sig P1 in
-    let '(x2, y2) := proj1_sig P2 in
-    (1 + d*x1*x2*y1*y2) <> 0.
-    (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
-  Admitted.
-  Lemma twistedAddCompleteMinus : forall (P1 P2:point),
-    let '(x1, y1) := proj1_sig P1 in
-    let '(x2, y2) := proj1_sig P2 in
-    (1 - d*x1*x2*y1*y2) <> 0.
-    (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
-  Admitted.
 
   Lemma point_eq : forall x1 x2 y1 y2,
     x1 = x2 -> y1 = y2 ->
@@ -199,7 +348,7 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
   Proof.
     intros; subst; f_equal.
     apply (UIP_dec). (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
-    admit. (* GF_eq_dec *)
+    apply GF_eq_dec.
   Qed.
   Hint Resolve point_eq.
 
@@ -221,7 +370,12 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
     (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
   Admitted.
 
+  Lemma zeroIsIdentity' : forall P, unifiedAdd' P (proj1_sig zero) = P.
+    unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field; auto.
+  Qed.
+
   Lemma zeroIsIdentity : forall P, P + zero = P.
+    (* Should follow from zeroIsIdentity', but dependent types... *)
   Admitted.
   Hint Resolve zeroIsIdentity.
 
@@ -353,11 +507,12 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
 End CompleteTwistedEdwardsFacts.
 
 Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
-  Module Export GFDefs := GaloisDefs M.
+  Module Export GFDefs := ZGaloisField M.
   Local Open Scope GF_scope.
+  Axiom char_gt_2 : inject 2 <> 0.
   Definition a := inject (- 1).
   Axiom a_nonzero : a <> 0.
-  Axiom a_square : exists x, x * x = a.
+  Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End Minus1Params.
@@ -382,12 +537,14 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Hint Unfold projectiveToTwisted twistedToProjective.
 
   Lemma GFdiv_1 : forall x, x/1 = x.
-  Admitted.
+  Proof.
+    intros; field; auto.
+  Qed.
   Hint Resolve GFdiv_1.
 
   Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P.
   Proof.
-    twisted; eapply GFdiv_1.
+    twisted; eauto.
   Qed.
 
   (** [extended] represents a point on an elliptic curve using extended projective
@@ -397,13 +554,7 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Definition point := extended.
   Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T).
   Definition extendedValid (P : point) : Prop :=
-    let pP := extendedToProjective P in
-    let X := projectiveX pP in
-    let Y := projectiveY pP in
-    let Z := projectiveZ pP in
-    let T := extendedT P in
-    T = X*Y/Z.
-
+    let '(X, Y, Z, T) := P in T = X*Y/Z.
 
   Definition twistedToExtended (P : (GF*GF)) : point :=
     let '(x, y) := P in (x, y, 1, x*y).
@@ -450,21 +601,12 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
   Local Notation "2" := (1+1).
   (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
   Definition unifiedAdd (P1 P2 : point) : point :=
-    let k := 2 * d in
-    let pP1 := extendedToProjective P1 in
-    let X1 := projectiveX pP1 in
-    let Y1 := projectiveY pP1 in
-    let Z1 := projectiveZ pP1 in
-    let T1 := extendedT P1 in
-    let pP2 := extendedToProjective P2 in
-    let X2 := projectiveX pP2 in
-    let Y2 := projectiveY pP2 in
-    let Z2 := projectiveZ pP2 in
-    let T2 := extendedT P2 in
+    let '(X1, Y1, Z1, T1) := P1 in
+    let '(X2, Y2, Z2, T2) := P2 in
     let  A := (Y1-X1)*(Y2-X2) in
     let  B := (Y1+X1)*(Y2+X2) in
-    let  C := T1*k*T2 in
-    let  D := Z1*2*Z2 in
+    let  C := T1*2*d*T2 in
+    let  D := Z1*2  *Z2 in
     let  E := B-A in
     let  F := D-C in
     let  G := D+C in
@@ -487,22 +629,9 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted
     destruct P1 as [[X1 Y1 Z1] T1].
     destruct P2 as [[X2 Y2 Z2] T2].
     destruct P3 as [[X3 Y3 Z3] T3].
-    unfold extendedValid, extendedToProjective, projectiveToTwisted in *.
     invcs HeqP3.
-    subst.
-    (* field. -- fails. but it works in sage:
-sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2");
-print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) ==
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-(2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) /
-((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-(2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))'
-      Outputs:
-        True
-    *)
+    field.
+    (* TODO: prove that denominators are nonzero *)
   Admitted.
 
   Ltac extended0 := repeat progress (autounfold; simpl); intros;
diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v
index af4f892ca..de26c678c 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -1,7 +1,7 @@
 Require Import ZArith NPeano.
 Require Import Bedrock.Word.
 Require Import Crypto.Curves.PointFormats.
-Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
+Require Import Crypto.Galois.BaseSystem Crypto.Galois.ZGaloisField Crypto.Galois.GaloisTheory.
 Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
 
@@ -54,7 +54,7 @@ Module Type EdDSAParams.
   Axiom n_ge_c : n >= c.
   Axiom n_le_b : n <= b.
 
-  Module Import GFDefs := GaloisDefs Modulus_q.
+  Module Import GFDefs := ZGaloisField Modulus_q.
   Local Open Scope GF_scope.
 
   (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit
@@ -83,6 +83,8 @@ Module Type EdDSAParams.
    *   twisted Edwards addition law. *)
   Module CurveParameters <: TwistedEdwardsParams Modulus_q.
     Module GFDefs := GFDefs.
+    Definition char_gt_2 : inject 2 <> 0.
+    Admitted. (* follows from q_odd *)
     Definition a : GF := a.
     Definition a_nonzero := a_nonzero.
     Definition a_square := a_square.
diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v
index 3ee86e4e4..4fd151d36 100644
--- a/src/Galois/Galois.v
+++ b/src/Galois/Galois.v
@@ -53,6 +53,13 @@ Module Galois (M: Modulus).
               apply prime_ge_2 in p; intuition).
   Defined.
 
+  Lemma GFone_nonzero : GFone <> GFzero.
+  Proof.
+    unfold GFone, GFzero.
+    intuition; solve_by_inversion.
+  Qed.
+  Hint Resolve GFone_nonzero.
+
   Definition GFplus(x y: GF): GF.
     exists ((x + y) mod modulus);
     abstract (rewrite Zmod_mod; trivial).
diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v
index f649701b7..12bcfa2c8 100644
--- a/src/Galois/GaloisExamples.v
+++ b/src/Galois/GaloisExamples.v
@@ -42,6 +42,12 @@ Module Example31.
     field; trivial.
   Qed.
 
+  Lemma example4: forall x: GF, x/(inject 1) = x.
+  Proof.
+    intros; field.
+    discriminate.
+  Qed.
+
 End Example31.
 
 Module TimesZeroTransparentTestModule.
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v
index bf9efa964..a554e826a 100644
--- a/src/Galois/ZGaloisField.v
+++ b/src/Galois/ZGaloisField.v
@@ -1,7 +1,7 @@
-
 Require Import BinInt BinNat ZArith Znumtheory.
 Require Import BoolEq Field_theory.
 Require Import Galois GaloisTheory.
+Require Import Tactics.VerdiTactics.
 
 Module ZGaloisField (M: Modulus).
   Module G := Galois M.
@@ -52,11 +52,20 @@ Module ZGaloisField (M: Modulus).
       apply prime_ge_2 in p; intuition.
   Qed.
 
+  Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
+  Proof.
+    intuition; solve_by_inversion.
+  Qed.
+
   Ltac GFpreprocess :=
     repeat rewrite injectZeroIsGFZero;
     repeat rewrite injectOneIsGFOne.
 
   Ltac GFpostprocess :=
+    repeat split;
+		repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
+			replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
+		end;
     repeat rewrite <- injectZeroIsGFZero;
     repeat rewrite <- injectOneIsGFOne.
 
@@ -79,6 +88,4 @@ Module ZGaloisField (M: Modulus).
      constants [GFconstant],
      div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]). 
-
 End ZGaloisField.
-
diff --git a/src/Scratch/fermat.v b/src/Scratch/fermat.v
index 7871db92f..947ffce15 100644
--- a/src/Scratch/fermat.v
+++ b/src/Scratch/fermat.v
@@ -42,7 +42,7 @@ Section Fq.
 
   Axiom inv : Fq -> Fq.
   Axiom inv_spec : forall a, inv a * a = one.
-  Definition div a b := add a (inv b).
+  Definition div a b := mul a (inv b).
   Infix "/" := div.
 
   Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 235c34a9b..51f1b14c8 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -6,17 +6,24 @@ Require Import QArith.QArith QArith.Qround.
 Require Import VerdiTactics.
 Close Scope Q.
 
+Ltac twoIndices i j base := 
+    intros;
+    assert (In i (seq 0 (length base))) by nth_tac;
+    assert (In j (seq 0 (length base))) by nth_tac;
+    repeat match goal with [ x := _ |- _ ] => subst x end;
+    simpl in *; repeat break_or_hyp; try omega; vm_compute; reflexivity.
+
 Module Base25Point5_10limbs <: BaseCoefs.
   Local Open Scope Z_scope.
   Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
   Lemma base_positive : forall b, In b base -> b > 0.
   Proof.
-    compute; intros; repeat break_or_hyp; intuition.
+    compute; intuition; subst; intuition.
   Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma base_good :
@@ -25,11 +32,7 @@ Module Base25Point5_10limbs <: BaseCoefs.
     let r := (b i * b j) / b (i+j)%nat in
     b i * b j = r * b (i+j)%nat.
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In j (seq 0 (length base))) by nth_tac.
-    subst b; subst r; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    twoIndices i j base.
   Qed.
 End Base25Point5_10limbs.
 
@@ -53,7 +56,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
   Lemma modulus_pseudomersenne :
     primeToZ modulus = 2^k - c.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma base_matches_modulus :
@@ -65,59 +68,65 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb
     let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
               b i * b j = r * (2^k * b (i+j-length base)%nat).
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In j (seq 0 (length base))) by nth_tac.
-    subst b; subst r; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    twoIndices i j base.
   Qed.
 
   Lemma base_succ : forall i, ((S i) < length base)%nat -> 
     let b := nth_default 0 base in
     b (S i) mod b i = 0.
   Proof.
-    intros.
-    assert (In i (seq 0 (length base))) by nth_tac.
-    assert (In (S i) (seq 0 (length base))) by nth_tac.
-    subst b; simpl in *.
-    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+    intros; twoIndices i (S i) base.
   Qed.
 
   Lemma base_tail_matches_modulus:
     2^k mod nth_default 0 base (pred (length base)) = 0.
   Proof.
-    nth_tac.
+    auto.
   Qed.
 
   Lemma b0_1 : forall x, nth_default x base 0 = 1.
   Proof.
-    reflexivity.
+    auto.
   Qed.
 
   Lemma k_nonneg : 0 <= k.
   Proof.
-    rewrite Zle_is_le_bool; reflexivity.
+    rewrite Zle_is_le_bool; auto.
   Qed.
 End GF25519Base25Point5Params.
 
 Module GF25519Base25Point5 := GFPseudoMersenneBase Base25Point5_10limbs Modulus25519 GF25519Base25Point5Params.
 
-Ltac expand_list f :=
-  assert ((length f < 100)%nat) as _ by (simpl length in *; omega);
-    repeat progress (
-    let n := fresh f in
-    destruct f as [ | n ];
-    try solve [simpl length in *; try discriminate]).
-
-(* TODO: move to ListUtil *)
-Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
-Proof.
-  intros; solve_by_inversion.
-Qed.
-Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys.
-Proof.
-  intros; solve_by_inversion.
-Qed.
+Ltac expand_list ls :=
+  let Hlen := fresh "Hlen" in
+  match goal with [H: ls = ?lsdef |- _ ] =>
+      assert (Hlen:length ls=length lsdef) by (f_equal; exact H)
+  end;
+  simpl in Hlen;
+  repeat progress (let n:=fresh ls in destruct ls as [|n ]; try solve [revert Hlen; clear; discriminate]);
+  clear Hlen.
+
+Ltac letify r :=
+  match goal with
+  | [ H' : r = _ |- _ ] =>
+    match goal with
+    | [ H : ?x = ?e |- _ ] =>
+      is_var x;
+      match goal with (* only letify equations that appear nowhere other than r *)
+      | _ => clear H H' x; fail 1
+      | _ => fail 2
+      end || idtac;
+      pattern x in H';
+      match type of H' with
+      | (fun z => r = @?e' z) x =>
+        let H'' := fresh "H" in
+        assert (H'' : r = let x := e in e' x) by
+          (* congruence is slower for every subsequent letify *)
+          (rewrite H'; subst x; reflexivity);
+        clear H'; subst x; rename H'' into H'; cbv beta in H'
+      end
+    end
+  end.
 
 Ltac expand_list_equalities := repeat match goal with
   | [H: (?x::?xs = ?y::?ys) |- _ ] =>
@@ -129,10 +138,80 @@ Ltac expand_list_equalities := repeat match goal with
 end.
 
 Section GF25519Base25Point5Formula.
-  Local Open Scope Z_scope.
   Import GF25519Base25Point5.
   Import GF.
 
+  Hint Rewrite
+    Z.mul_0_l
+    Z.mul_0_r
+    Z.mul_1_l
+    Z.mul_1_r
+    Z.add_0_l
+    Z.add_0_r
+    Z.add_assoc
+    Z.mul_assoc
+    : Z_identities.
+
+  Ltac deriveModularMultiplicationWithCarries carryscript :=
+  let h := fresh "h" in
+  let fg := fresh "fg" in
+  let Hfg := fresh "Hfg" in
+  intros;
+  repeat match goal with
+  | [ Hf: rep ?fs ?f, Hg: rep ?gs ?g |- rep _ ?ret ] =>
+      remember (carry_sequence carryscript (mul fs gs)) as fg;
+      assert (rep fg ret) as Hfg; [subst fg; apply carry_sequence_rep, mul_rep; eauto|]
+  | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition)
+  | [ Heqfg: fg = carry_sequence _ (mul _ _) |- rep _ ?ret ] =>
+      (* expand bignum multiplication *)
+      cbv [plus
+        seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error
+        mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c
+        E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg;
+      repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *)
+          let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end;
+      autorewrite with Z_identities in Heqfg;
+      (* speparate out carries *)
+      match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end;
+      (* one equation per limb *)
+      expand_list h; expand_list_equalities;
+      (* expand carry *)
+      cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg
+  | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
+  | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *)
+      let cr := fresh "cr" in
+      remember (carry i (x::xs)) as cr in Hfg;
+      match goal with [ Heq : cr = ?crdef |- _ ] =>
+          (* is there any simpler way to do this? *)
+          cbv [carry carry_simple carry_and_reduce] in Heq;
+          simpl eq_nat_dec in Heq; cbv iota beta in Heq;
+          cbv [set_nth nth_default nth_error value add_to_nth] in Heq;
+          expand_list cr; expand_list_equalities
+      end
+  | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H;
+      match goal with [Heqc: c = cap i |- _ ] =>
+          (* is there any simpler way to do this? *)
+          unfold cap, Base25Point5_10limbs.base in Heqc;
+          simpl eq_nat_dec in Heqc;
+          cbv [nth_default nth_error value error] in Heqc;
+          simpl map in Heqc;
+          cbv [GF25519Base25Point5Params.k] in Heqc
+      end;
+      subst c;
+      repeat rewrite Zdiv_1_r in H;
+      repeat rewrite two_power_pos_equiv in H;
+      repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder));
+      repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity));
+      repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity));
+      simpl Z.sub in H;
+      unfold  GF25519Base25Point5Params.c in H
+  | [H: context[Z.ones ?l] |- _ ] =>
+          (* postponing this to the main loop makes the autorewrite slow *)
+        let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c
+  | [ |- _ ] => abstract (solve [auto])
+  | [ |- _ ] => progress intros
+  end.
+
   Lemma GF25519Base25Point5_mul_reduce_formula :
     forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 
       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
@@ -140,171 +219,14 @@ Section GF25519Base25Point5Formula.
                         -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
                         -> rep ls (f*g)%GF}.
   Proof.
-    intros.
-    eexists.
-    intros f g Hf Hg.
 
-    pose proof (mul_rep _ _  _ _ Hf Hg) as HmulRef.
-    remember (GF25519Base25Point5.mul [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9]) as h.
-    unfold
-      GF25519Base25Point5.mul,
-      GF25519Base25Point5.B.add,
-      GF25519Base25Point5.E.mul,
-      GF25519Base25Point5.E.mul',
-      GF25519Base25Point5.E.mul_bi,
-      GF25519Base25Point5.E.mul_bi',
-      GF25519Base25Point5.E.mul_each,
-      GF25519Base25Point5.E.add,
-      GF25519Base25Point5.B.digits,
-      GF25519Base25Point5.E.digits,
-      Base25Point5_10limbs.base,
-      GF25519Base25Point5.E.crosscoef,
-      nth_default
-    in Heqh; simpl in Heqh.
-
-    unfold
-      two_power_pos,
-      shift_pos
-    in Heqh; simpl in Heqh.
-
-    (* evaluate row-column crossing coefficients for variable base multiplication *)
-    (* unfoldZ.div in Heqh; simpl in Heqh. *) (* THIS TAKES TOO LONG *)
-    repeat rewrite Z_div_same_full in Heqh by (abstract (apply Zeq_bool_neq; reflexivity)).
-    repeat match goal with [ Heqh : context[ (?a / ?b)%Z ]  |- _ ] =>
-      replace (a / b)%Z with 2%Z in Heqh by
-        (abstract (symmetry; erewrite <- Z.div_unique_exact; try apply Zeq_bool_neq; reflexivity))
-    end.
-
-    Hint Rewrite
-      Z.mul_0_l
-      Z.mul_0_r
-      Z.mul_1_l
-      Z.mul_1_r
-      Z.add_0_l
-      Z.add_0_r
-      : Z_identities.
-    autorewrite with Z_identities in Heqh.
-
-    (* inline explicit formulas for modular reduction *)
-    cbv beta iota zeta delta [GF25519Base25Point5.reduce Base25Point5_10limbs.base] in Heqh.
-    remember GF25519Base25Point5Params.c as c in Heqh; unfold GF25519Base25Point5Params.c in Heqc.
-    simpl in Heqh.
+    eexists.
 
-    (* prettify resulting modular multiplication expression *)
-    repeat rewrite (Z.mul_add_distr_l c) in Heqh.
-    repeat rewrite (Z.mul_assoc _ _ 2) in Heqh.
-    repeat rewrite (Z.mul_comm _ 2) in Heqh.
-    repeat rewrite (Z.mul_assoc 2 c) in Heqh.
-    remember (2 * c)%Z as TwoC in Heqh; subst c; simpl in HeqTwoC; subst TwoC. (* perform operations on constants *)
-    repeat rewrite Z.add_assoc in Heqh.
-    repeat rewrite Z.mul_assoc in Heqh.
-    assert (Hhl: length h = 10%nat) by (subst h; reflexivity); expand_list h; clear Hhl.
-    expand_list_equalities.
+    Time deriveModularMultiplicationWithCarries (rev [0;1;2;3;4;5;6;7;8;9;0]).
     (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *)
-    (* output:
-      h0 = (f0*g0 + 38*f9*g1 + 19*f8*g2 + 38*f7*g3 + 19*f6*g4 + 38*f5*g5 + 19*f4*g6 + 38*f3*g7 + 19*f2*g8 + 38*f1*g9)
-      h1 = (f1*g0 + f0*g1    + 19*f9*g2 + 19*f8*g3 + 19*f7*g4 + 19*f6*g5 + 19*f5*g6 + 19*f4*g7 + 19*f3*g8 + 19*f2*g9)
-      h2 = (f2*g0 + 2*f1*g1  + f0*g2    + 38*f9*g3 + 19*f8*g4 + 38*f7*g5 + 19*f6*g6 + 38*f5*g7 + 19*f4*g8 + 38*f3*g9)
-      h3 = (f3*g0 + f2*g1    + f1*g2    + f0*g3    + 19*f9*g4 + 19*f8*g5 + 19*f7*g6 + 19*f6*g7 + 19*f5*g8 + 19*f4*g9)
-      h4 = (f4*g0 + 2*f3*g1  + f2*g2    + 2*f1*g3  + f0*g4    + 38*f9*g5 + 19*f8*g6 + 38*f7*g7 + 19*f6*g8 + 38*f5*g9)
-      h5 = (f5*g0 + f4*g1    + f3*g2    + f2*g3    + f1*g4    + f0*g5    + 19*f9*g6 + 19*f8*g7 + 19*f7*g8 + 19*f6*g9)
-      h6 = (f6*g0 + 2*f5*g1  + f4*g2    + 2*f3*g3  + f2*g4    + 2*f1*g5  + f0*g6    + 38*f9*g7 + 19*f8*g8 + 38*f7*g9)
-      h7 = (f7*g0 + f6*g1    + f5*g2    + f4*g3    + f3*g4    + f2*g5    + f1*g6    + f0*g7    + 19*f9*g8 + 19*f8*g9)
-      h8 = (f8*g0 + 2*f7*g1  + f6*g2    + 2*f5*g3  + f4*g4    + 2*f3*g5  + f2*g6    + 2*f1*g7  + f0*g8    + 38*f9*g9)
-      h9 = (f9*g0 + f8*g1    + f7*g2    + f6*g3    + f5*g4    + f4*g5    + f3*g6    + f2*g7    + f1*g8    + f0*g9)
-    *)
-    
-    (* prove equivalence of multiplication to the stated *)
-    assert (rep [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9] (f * g)%GF) as Hh. {
-      subst h0. subst h1. subst h2. subst h3. subst h4. subst h5. subst h6. subst h7. subst h8. subst h9.
-      repeat match goal with [H: _ = _ |- _ ] =>
-          rewrite <- H; clear H
-      end.
-      assumption.
-    }
 
-    (* --- carry phase --- *)
-    remember (rev [0;1;2;3;4;5;6;7;8;9;0])%nat as is; simpl in Heqis.
-    destruct (fun pf pf2 => carry_sequence_rep is _ _ pf pf2 Hh). {
-      subst is. clear. intros. simpl in *. firstorder.
-    } {
-      reflexivity.
-    }
-    remember (carry_sequence is [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9]) as r; subst is.
-
-    (* unroll the carry loop, create a separate variable for each of the 10 list elements *)
-    cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqr.
-    repeat match goal with
-    | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a
-    | [H: context[GF25519Base25Point5.carry ?i (?x::?xs)] |- _ ] =>
-        let cr := fresh "cr" in
-        remember (GF25519Base25Point5.carry i (x::xs)) as cr;
-        match goal with [ Heq : cr = ?crdef |- _ ] =>
-            cbv [GF25519Base25Point5.carry GF25519Base25Point5.carry_simple GF25519Base25Point5.carry_and_reduce] in Heq;
-            simpl eq_nat_dec in Heq; cbv iota beta in Heq;
-            cbv [set_nth nth_default nth_error value GF25519Base25Point5.add_to_nth] in Heq;
-            let Heql := fresh "Heql" in
-              assert (length cr = length crdef) as Heql by (subst cr; reflexivity);
-              simpl length in Heql; expand_list cr; clear Heql;
-            expand_list_equalities
-        end
-    end.
-
-    (* compute the human-meaningful froms of constants used during carrying *)
-    cbv [GF25519Base25Point5.cap Base25Point5_10limbs.base GF25519Base25Point5Params.k] in *.
-    simpl eq_nat_dec in *; cbv iota in *.
-    repeat match goal with
-    | [H: _ |- _ ] =>
-      rewrite (map_nth_default _ _ _ _ 0%nat 0%Z) in H by (abstract (clear; rewrite seq_length; firstorder))
-    end.
-    simpl two_p in *.
-    repeat rewrite two_power_pos_equiv in *.
-    repeat rewrite <- Z.pow_sub_r in * by (abstract (clear; firstorder)).
-    simpl Z.sub in *;
-    rewrite Zdiv_1_r in *.
-
-    (* replace division and Z.modulo with bit operations *)
-    remember (2 ^ 25)%Z as t25 in *.
-    remember (2 ^ 26)%Z as t26 in *.
-    repeat match goal with [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a end.
-    subst t25. subst t26.
-    rewrite <- Z.land_ones in * by (abstract (clear; firstorder)).
-    rewrite <- Z.shiftr_div_pow2 in * by (abstract (clear; firstorder)).
-
-    (* evaluate the constant arguments to bit operations *)
-    remember (Z.ones 25) as m25 in *. compute in Heqm25. subst m25.
-    remember (Z.ones 26) as m26 in *. compute in Heqm26. subst m26.
-    unfold GF25519Base25Point5Params.c in *.
-
-    (* This tactic takes in [r], a variable that we want to use to instantiate an existential.
-     * We find one other variable mentioned in [r], with its own equality in the hypotheses.
-     * That equality is then switched into a [let] in [r]'s defining equation. *)
-    Ltac letify r :=
-      match goal with
-      | [ H : ?x = ?e |- _ ] =>
-        is_var x;
-        match goal with
-        | [ H' : r = _ |- _ ] =>
-          pattern x in H';
-            match type of H' with
-            | (fun z => r = @?e' z) x =>
-              let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence;
-                clear H'; subst x; rename H'' into H'; cbv beta in H'
-            end
-        end
-      end.
-
-    (* To instantiate an existential, give a variable with a defining equation to this tactic.
-     * We instantiate with a [let]-ified version of that equation. *)
-    Ltac existsFromEquations r := repeat letify r;
-                                 match goal with
-                                 | [ _ : r = ?e |- context[?u] ] => unify u e
-                                 end.
-
-    clear HmulRef Hh Hf Hg.
-    existsFromEquations r.
-    split; auto; congruence.
-  Defined.
+    Time repeat letify fg; subst fg; eauto.
+  Time Defined.
 End GF25519Base25Point5Formula.
 
 Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
@@ -312,3 +234,6 @@ Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
  * More Ltac acrobatics will be needed to get out that formula for further use in Coq.
  * The easiest fix will be to make the proof script above fully automated,
  * using [abstract] to contain the proof part. *)
+
+
+
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 350f55dd8..783e3f527 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -524,3 +524,12 @@ Ltac set_nth_inbounds :=
   end.
 
 Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds.
+
+Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
+Proof.
+  intros; solve_by_inversion.
+Qed.
+Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys.
+Proof.
+  intros; solve_by_inversion.
+Qed.