Prove relationship between `xzladderstep` and M.add (#162)

* hopefully all proofs we need about xzladderstep

* Better automation in xzproofs

* Speed up xzproofs with heuristic clearing

* Remove useless hypotheses

* XZProofs cleanup

* fix "group by isomorphism" proofs, use in XZProofs

13 files changed, 421 insertions, 324 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index 7270f6018..b5b65f161 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -186,7 +186,7 @@ Section Homomorphism_rev.
            | [ H : field |- _ ] => destruct H; try clear H
            | [ H : commutative_ring |- _ ] => destruct H; try clear H
            | [ H : ring |- _ ] => destruct H; try clear H
-           | [ H : abelian_group |- _ ] => destruct H; try clear H
+           | [ H : commutative_group |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
            | [ H : monoid |- _ ] => destruct H; try clear H
            | [ H : is_commutative |- _ ] => destruct H; try clear H
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 8ce3e2a91..27c45dcec 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -104,24 +104,35 @@ Section Homomorphism.
   End ScalarMultHomomorphism.
 End Homomorphism.
 
-Section Homomorphism_rev.
-  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
+Section GroupByIsomorphism.
+  Context {G} {EQ:G->G->Prop} {OP:G->G->G} {ID:G} {INV:G->G}.
   Context {H} {eq : H -> H -> Prop} {op : H -> H -> H} {id : H} {inv : H -> H}.
   Context {phi:G->H} {phi':H->G}.
   Local Infix "=" := EQ. Local Infix "=" := EQ : type_scope.
-  Context (phi'_phi_id : forall A, phi' (phi A) = A)
-          (phi'_eq : forall a b, EQ (phi' a) (phi' b) <-> eq a b)
-          (phi'_op : forall a b, phi' (op a b) = OP (phi' a) (phi' b))
-          {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
-          {phi'_id : phi' id = ID}.
-
-  Lemma group_from_redundant_representation
-    : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'.
+
+  Class isomorphic_groups :=
+    {
+      isomorphic_groups_group_G :> @group G EQ OP ID INV;
+      isomorphic_groups_group_H :> @group H eq op id inv;
+      isomorphic_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
+      isomorphic_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
+    }.
+
+  Lemma group_by_isomorphism
+        (groupG:@group G EQ OP ID INV)
+        (phi'_phi_id : forall A, phi' (phi A) = A)
+        (phi'_eq : forall a b, EQ (phi' a) (phi' b) <-> eq a b)
+        (phi'_op : forall a b, phi' (op a b) = OP (phi' a) (phi' b))
+        (phi'_inv : forall a, phi' (inv a) = INV (phi' a))
+        (phi'_id : phi' id = ID)
+    : isomorphic_groups.
   Proof using Type*.
     repeat match goal with
            | [ H : _/\_ |- _ ] => destruct H; try clear H
+           | [ H : commutative_group |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
            | [ H : monoid |- _ ] => destruct H; try clear H
+           | [ H : is_commutative |- _ ] => destruct H; try clear H
            | [ H : is_associative |- _ ] => destruct H; try clear H
            | [ H : is_left_identity |- _ ] => destruct H; try clear H
            | [ H : is_right_identity |- _ ] => destruct H; try clear H
@@ -138,79 +149,51 @@ Section Homomorphism_rev.
            | _ => solve [ eauto ]
            end.
   Qed.
+End GroupByIsomorphism.
 
-  Definition homomorphism_from_redundant_representation
-    : @Monoid.is_homomorphism G EQ OP H eq op phi.
-  Proof using groupG phi'_eq phi'_op phi'_phi_id.
-    split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy.
-  Qed.
-End Homomorphism_rev.
-
-Section GroupByHomomorphism.
-  Lemma surjective_homomorphism_from_group
-        {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}
-        {H eq op id inv}
-        {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} }
-        {Proper_op:Proper(eq==>eq==>eq)op}
-        {Proper_inv:Proper(eq==>eq)inv}
-        {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
-        {surj:forall h, eq (phi (iph h)) h}
-        {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
-        {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
-        {phi_id : eq (phi ID) id}
-  : @group H eq op id inv.
-  Proof.
-    repeat split; eauto with core typeclass_instances; intros;
-      repeat match goal with
-               |- context[?x] =>
-               match goal with
-               | |- context[iph x] => fail 1
-               | _ => unify x id; fail 1
-               | _ => is_var x; rewrite <- (surj x)
-               end
-             end;
-      repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id;
-      f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse.
-  Qed.
-
-  Lemma isomorphism_to_subgroup_group
-        {G EQ OP ID INV}
-        {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
-        {Proper_OP:Proper(EQ==>EQ==>EQ)OP}
-        {Proper_INV:Proper(EQ==>EQ)INV}
-        {H eq op id inv} {groupG:@group H eq op id inv}
-        {phi}
-        {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
-        {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
-        {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
-        {phi_id : eq (phi ID) id}
-    : @group G EQ OP ID INV.
-  Proof.
-    repeat split; eauto with core typeclass_instances; intros;
-      eapply eq_phi_EQ;
-      repeat rewrite ?phi_op, ?phi_inv, ?phi_id;
-      auto using associative, left_identity, right_identity, left_inverse, right_inverse.
-  Qed.
-End GroupByHomomorphism.
+Section CommutativeGroupByIsomorphism.
+  Context {G} {EQ:G->G->Prop} {OP:G->G->G} {ID:G} {INV:G->G}.
+  Context {H} {eq : H -> H -> Prop} {op : H -> H -> H} {id : H} {inv : H -> H}.
+  Context {phi:G->H} {phi':H->G}.
+  Local Infix "=" := EQ. Local Infix "=" := EQ : type_scope.
 
-Section HomomorphismComposition.
-  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
-  Context {H eq op id inv} {groupH:@group H eq op id inv}.
-  Context {K eqK opK idK invK} {groupK:@group K eqK opK idK invK}.
-  Context {phi:G->H} {phi':H->K}
-          {Hphi:@Monoid.is_homomorphism G EQ OP H eq op phi}
-          {Hphi':@Monoid.is_homomorphism H eq op K eqK opK phi'}.
-  Lemma is_homomorphism_compose
-        {phi'':G->K}
-        (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
-    : @Monoid.is_homomorphism G EQ OP K eqK opK phi''.
-  Proof using Hphi Hphi' groupK.
-    split; repeat intro; rewrite <- !Hphi''.
-    { rewrite !Monoid.homomorphism; reflexivity. }
-    { apply Hphi', Hphi; assumption. }
+  Class isomorphic_commutative_groups :=
+    {
+      isomorphic_commutative_groups_group_G :> @commutative_group G EQ OP ID INV;
+      isomorphic_commutative_groups_group_H :> @commutative_group H eq op id inv;
+      isomorphic_commutative_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
+      isomorphic_commutative_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
+    }.
+
+  Lemma commutative_group_by_isomorphism
+        (groupG:@commutative_group G EQ OP ID INV)
+        (phi'_phi_id : forall A, phi' (phi A) = A)
+        (phi'_eq : forall a b, EQ (phi' a) (phi' b) <-> eq a b)
+        (phi'_op : forall a b, phi' (op a b) = OP (phi' a) (phi' b))
+        (phi'_inv : forall a, phi' (inv a) = INV (phi' a))
+        (phi'_id : phi' id = ID)
+    : isomorphic_commutative_groups.
+  Proof using Type*.
+    repeat match goal with
+           | [ H : _/\_ |- _ ] => destruct H; try clear H
+           | [ H : commutative_group |- _ ] => destruct H; try clear H
+           | [ H : group |- _ ] => destruct H; try clear H
+           | [ H : monoid |- _ ] => destruct H; try clear H
+           | [ H : is_commutative |- _ ] => destruct H; try clear H
+           | [ H : is_associative |- _ ] => destruct H; try clear H
+           | [ H : is_left_identity |- _ ] => destruct H; try clear H
+           | [ H : is_right_identity |- _ ] => destruct H; try clear H
+           | [ H : Equivalence _ |- _ ] => destruct H; try clear H
+           | [ H : is_left_inverse |- _ ] => destruct H; try clear H
+           | [ H : is_right_inverse |- _ ] => destruct H; try clear H
+           | _ => intro
+           | _ => split
+           | [ H : eq _ _ |- _ ] => apply phi'_eq in H
+           | [ |- eq _ _ ] => apply phi'_eq
+           | [ H : EQ _ _ |- _ ] => rewrite H
+           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity
+           | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity
+           | _ => solve [ eauto ]
+           end.
   Qed.
-
-  Global Instance is_homomorphism_compose_refl
-    : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
-    := is_homomorphism_compose (fun x => reflexivity _).
-End HomomorphismComposition.
+End CommutativeGroupByIsomorphism.
\ No newline at end of file
diff --git a/src/Algebra/Hierarchy.v b/src/Algebra/Hierarchy.v
index 342e9feaa..07f1f30fd 100644
--- a/src/Algebra/Hierarchy.v
+++ b/src/Algebra/Hierarchy.v
@@ -57,14 +57,14 @@ Section Algebra.
 
     Class is_commutative := { commutative : forall x y, op x y = op y x }.
 
-    Record abelian_group :=
+    Record commutative_group :=
       {
-        abelian_group_group : group;
-        abelian_group_is_commutative : is_commutative
+        commutative_group_group : group;
+        commutative_group_is_commutative : is_commutative
       }.
-    Existing Class abelian_group.
-    Global Existing Instance abelian_group_group.
-    Global Existing Instance abelian_group_is_commutative.
+    Existing Class commutative_group.
+    Global Existing Instance commutative_group_group.
+    Global Existing Instance commutative_group_is_commutative.
   End SingleOperation.
 
   Section AddMul.
@@ -79,7 +79,7 @@ Section Algebra.
 
     Class ring :=
       {
-        ring_abelian_group_add : abelian_group (op:=add) (id:=zero) (inv:=opp);
+        ring_commutative_group_add : commutative_group (op:=add) (id:=zero) (inv:=opp);
         ring_monoid_mul : monoid (op:=mul) (id:=one);
         ring_is_left_distributive : is_left_distributive;
         ring_is_right_distributive : is_right_distributive;
@@ -89,7 +89,7 @@ Section Algebra.
         ring_mul_Proper : Proper (respectful eq (respectful eq eq)) mul;
         ring_sub_Proper : Proper(respectful eq (respectful eq eq)) sub
       }.
-    Global Existing Instance ring_abelian_group_add.
+    Global Existing Instance ring_commutative_group_add.
     Global Existing Instance ring_monoid_mul.
     Global Existing Instance ring_is_left_distributive.
     Global Existing Instance ring_is_right_distributive.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index 470e8df40..e5755b6f0 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -58,3 +58,25 @@ Section Homomorphism.
     }.
   Global Existing Instance is_homomorphism_phi_proper.
 End Homomorphism.
+
+Section HomomorphismComposition.
+  Context {G EQ OP ID} {monoidG:@monoid G EQ OP ID}.
+  Context {H eq op id} {monoidH:@monoid H eq op id}.
+  Context {K eqK opK idK} {monoidK:@monoid K eqK opK idK}.
+  Context {phi:G->H} {phi':H->K}
+          {Hphi:@is_homomorphism G EQ OP H eq op phi}
+          {Hphi':@is_homomorphism H eq op K eqK opK phi'}.
+  Lemma is_homomorphism_compose
+        {phi'':G->K}
+        (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
+    : @is_homomorphism G EQ OP K eqK opK phi''.
+  Proof using Hphi Hphi' monoidK.
+    split; repeat intro; rewrite <- !Hphi''.
+    { rewrite !homomorphism; reflexivity. }
+    { apply Hphi', Hphi; assumption. }
+  Qed.
+
+  Global Instance is_homomorphism_compose_refl
+    : @is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
+    := is_homomorphism_compose (fun x => reflexivity _).
+End HomomorphismComposition.
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index 406706988..2e3bcba58 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -205,7 +205,7 @@ Section Isomorphism.
            | [ H : field |- _ ] => destruct H; try clear H
            | [ H : commutative_ring |- _ ] => destruct H; try clear H
            | [ H : ring |- _ ] => destruct H; try clear H
-           | [ H : abelian_group |- _ ] => destruct H; try clear H
+           | [ H : commutative_group |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
            | [ H : monoid |- _ ] => destruct H; try clear H
            | [ H : is_commutative |- _ ] => destruct H; try clear H
diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
index 2d1db7126..e77e39f50 100644
--- a/src/Curves/Edwards/AffineProofs.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -51,7 +51,7 @@ Module E.
       | _ => solve [trivial | exact _ ]
       | _ => intro
       | |- Equivalence _ => split
-      | |- abelian_group => split | |- group => split | |- monoid => split
+      | |- commutative_group => split | |- group => split | |- monoid => split
       | |- is_associative => split | |- is_commutative => split
       | |- is_left_inverse => split | |- is_right_inverse => split
       | |- is_left_identity => split | |- is_right_identity => split
@@ -80,7 +80,7 @@ Module E.
       { intro. eapply H0. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
     Qed.
 
-    Global Instance edwards_curve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
+    Global Instance edwards_curve_commutative_group : commutative_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof using Type. t. Qed.
 
     Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof using Type. repeat t_step. Qed.
diff --git a/src/Curves/Edwards/Montgomery.v b/src/Curves/Edwards/Montgomery.v
deleted file mode 100644
index d274356c9..000000000
--- a/src/Curves/Edwards/Montgomery.v
+++ /dev/null
@@ -1,114 +0,0 @@
-Require Import Crypto.Curves.Edwards.AffineProofs.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.AffineProofs.
-Require Import Crypto.Curves.Montgomery.Affine.
-
-Require Import Crypto.Util.Notations Crypto.Util.Decidable.
-Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
-Require Import Crypto.Algebra.Field.
-Import BinNums.
-
-Module E.
-  Section EdwardsMontgomery.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}
-            {Feq_dec:DecidableRel Feq}.
-    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
-    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^ 2" := (x*x).
-
-    Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
-    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
-
-    Context {a d: F}
-            {nonzero_a : a <> 0}
-            {square_a : exists sqrt_a, sqrt_a^2 = a}
-            {nonsquare_d : forall x, x^2 <> d}.
-    Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
-    Local Notation Ezero  := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
-    Local Notation Eadd   := (E.add(char_ge_3:=char_ge_3)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
-    Local Notation Eopp   := (E.opp(nonzero_a:=nonzero_a)(d:=d)).
-
-    Let a_neq_d : a <> d.
-    Proof. intro X.
-           edestruct square_a. eapply nonsquare_d.
-           rewrite <-X. eassumption. Qed.
-
-    
-    Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1).
-    Local Notation MontgomeryA := (2*(a+d)/(a-d)).
-    Local Notation MontgomeryB := (4/(a-d)).
-
-    Let b_nonzero : MontgomeryB <> 0. Proof. fsatz. Qed.
-
-    Local Notation Mpoint := (@M.point F Feq Fadd Fmul MontgomeryA MontgomeryB).
-    Local Notation Madd := (@M.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 MontgomeryA MontgomeryB b_nonzero).
-    Local Notation "'∞'" := (inr tt) : core_scope.
-
-    Ltac t_step :=
-        match goal with
-        | _ => solve [ contradiction | trivial ]
-        | _ => progress intros
-        | _ => progress subst
-        | _ => progress Tactics.DestructHead.destruct_head' @M.point
-        | _ => progress Tactics.DestructHead.destruct_head' @prod
-        | _ => progress Tactics.DestructHead.destruct_head' @sum
-        | _ => progress Tactics.DestructHead.destruct_head' @and
-        | _ => progress Sum.inversion_sum
-        | _ => progress Prod.inversion_prod
-        | _ => progress Tactics.BreakMatch.break_match_hyps
-        | _ => progress Tactics.BreakMatch.break_match
-        | _ => progress cbv [E.coordinates M.coordinates E.add M.add E.zero M.zero E.eq M.eq E.opp M.opp proj1_sig fst snd] in *
-        | |- _ /\ _ => split
-        end.
-    Ltac t := repeat t_step.
-
-    Program Definition to_Montgomery (P:Epoint) : Mpoint :=
-      match E.coordinates P return F*F+_ with
-      | (x, y) => 
-        if dec (y <> 1 /\ x <> 0)
-        then inl ((1+y)/(1-y), (1+y)/(x-x*y))
-        else ∞
-      end.
-    Next Obligation. Proof. t. fsatz. Qed.
-
-    (* The exceptional cases are tricky. *)
-    (* See https://eprint.iacr.org/2008/013.pdf page 5 before continuing *)
-
-    Program Definition of_Montgomery (P:Mpoint) : Epoint :=
-      match M.coordinates P return F*F with
-      | inl (x,y) =>
-        if dec (y = 0)
-        then (0, Fopp 1)
-        else (x/y, (x-1)/(x+1))
-      | ∞ => pair 0 1
-      end.
-    Next Obligation.
-    Proof.
-      t; try fsatz.
-      assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz.
-    Admitted.
-
-    Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ :=
-      @Group.group_from_redundant_representation
-        Mpoint M.eq Madd M.zero M.opp
-        (M.group discr_nonzero)
-        Epoint E.eq Eadd Ezero Eopp
-        of_Montgomery
-        to_Montgomery
-        _ _ _ _ _
-    .
-    Next Obligation. Proof. Admitted. (* M->E->M *)
-    Next Obligation. Proof. Admitted. (* equivalences match *)
-    Next Obligation. Proof. Admitted. (* add *)
-    Next Obligation. Proof. Admitted. (* opp *)
-    Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed.
-
-    Global Instance homomorphism_of_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)).
-    Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)).
-  End EdwardsMontgomery.
-End E.
diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
index 160866b64..2b126dfcb 100644
--- a/src/Curves/Edwards/XYZT.v
+++ b/src/Curves/Edwards/XYZT.v
@@ -107,34 +107,23 @@ Module Extended.
         end.
       Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
 
-      Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : Algebra.Hierarchy.group /\ _ /\ _ :=
-                 @Group.group_from_redundant_representation
-                   _ _ _ _ _
-                   ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a')
-                                                  (nonsquare_d:=nonsquare_d')).(Algebra.Hierarchy.abelian_group_group))
-                   _
-                   eq
-                   m1add
-                   zero
-                   opp
-                   from_twisted
-                   to_twisted
-                   to_twisted_from_twisted
-                   _ _ _ _.
-      Next Obligation. cbv [to_twisted]. t. Qed.
-      Next Obligation.
-        match goal with
-        | |- context[E.add ?P ?Q] =>
-          unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q))
-        end. cbv [to_twisted m1add]. t. Qed.
-      Next Obligation. cbv [to_twisted opp]. t. Qed.
-      Next Obligation. cbv [to_twisted zero]. t. Qed.
-      Global Instance group x y z
-        : Algebra.Hierarchy.group := proj1 (_group_proof x y z).
-      Global Instance homomorphism_from_twisted x y z :
-        Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)).
-      Global Instance homomorphism_to_twisted x y z :
-        Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)).
+      Global Instance isomorphic_commutative_group_m1 :
+        @Group.isomorphic_commutative_groups
+          Epoint E.eq
+            (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d))
+            (E.zero(nonzero_a:=nonzero_a))
+            (E.opp(nonzero_a:=nonzero_a))
+          point eq m1add zero opp
+          from_twisted to_twisted.
+      Proof.
+        eapply Group.commutative_group_by_isomorphism; try exact _.
+        par: abstract
+               (cbv [to_twisted from_twisted zero opp m1add]; intros;
+                repeat match goal with
+                       | |- context[E.add ?P ?Q] =>
+                         unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q)) end;
+                t).
+      Qed.
     End TwistMinusOne.
   End ExtendedCoordinates.
 End Extended.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index 721908a6a..70e8a3f6f 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -38,17 +38,15 @@ Module M.
     Section MontgomeryWeierstrass.
       Local Notation "2" := (1+1).
       Local Notation "3" := (1+2).
-      Local Notation "4" := (1+3).
-      Local Notation "16" := (4*4).
+      Local Notation "4" := (1+1+1+1).
       Local Notation "9" := (3*3).
-      Local Notation "27" := (3*9).
-      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+      Local Notation "27" := (4*4 + 4+4 +1+1+1).
 
+      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
 
-      Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
-      Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
-      Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
-      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+      Context {aw bw} {Haw:aw=(3-a^2)/(3*b^2)} {Hbw:bw=(2*a^3-9*a)/(27*b^3)}.
+      Local Notation Wpoint := (@W.point F Feq Fadd Fmul aw bw).
+      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 aw bw).
       Program Definition to_Weierstrass (P:@point) : Wpoint :=
         match M.coordinates P return F*F+∞ with
         | (x, y) => ((x + a/3)/b, y/b)
diff --git a/src/Curves/Montgomery/AffineInstances.v b/src/Curves/Montgomery/AffineInstances.v
new file mode 100644
index 000000000..ef5ccd578
--- /dev/null
+++ b/src/Curves/Montgomery/AffineInstances.v
@@ -0,0 +1,50 @@
+Require Import Crypto.Algebra.Field.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine.
+Require Import Crypto.Curves.Weierstrass.AffineProofs.
+Require Import Crypto.Curves.Montgomery.AffineProofs.
+Require Import Coq.Classes.RelationClasses.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "0" := Fzero.
+    Local Notation "1" := Fone.
+    Local Notation "4" := (1+1+1+1).
+      
+    Global Instance MontgomeryWeierstrassIsomorphism
+           {a b: F}
+           (b_nonzero : b <> 0)
+           (discriminant_nonzero: a^2 - 4 <> 0)
+           {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}
+           {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}
+           {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28} (* XXX: this is a workaround for nsatz assuming arbitrary characteristic *)
+      :
+      @Group.isomorphic_commutative_groups
+        (@W.point F Feq Fadd Fmul _ _)
+        W.eq
+        (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field _ char_ge_3 _ _)
+        W.zero
+        (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv _ _ field _)
+
+        (@M.point F Feq Fadd Fmul a b)
+        M.eq
+        (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero))
+        M.zero
+        (M.opp(b_nonzero:=b_nonzero))
+        
+        (M.of_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero))
+        (M.to_Weierstrass(Haw:=reflexivity _)(Hbw:=reflexivity _)(b_nonzero:=b_nonzero)).
+    Proof.
+      eapply @AffineProofs.M.MontgomeryWeierstrassIsomorphism; try assumption; cbv [id]; fsatz.
+    Qed.
+  End MontgomeryCurve.
+End M.
diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v
index a83109a55..4601c3b66 100644
--- a/src/Curves/Montgomery/AffineProofs.v
+++ b/src/Curves/Montgomery/AffineProofs.v
@@ -12,12 +12,7 @@ Module M.
     Import BinNat.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {Feq_dec:Decidable.DecidableRel Feq}
-            {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
-    Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
-    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+            {Feq_dec:Decidable.DecidableRel Feq}.
       
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
@@ -25,21 +20,22 @@ Module M.
     Local Notation "- x" := (Fopp x).
     Local Notation "x ^ 2" := (x*x) (at level 30).
     Local Notation "x ^ 3" := (x*x^2) (at level 30).
-    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Notation "2" := (1+1). Local Notation "3" := (1+2).
-    Local Notation "9" := (3*3). Local Notation "27" := (3*9).
+    Local Notation "0" := Fzero.
+    Local Notation "1" := Fone.
+    Local Notation "2" := (1+1).
+    Local Notation "3" := (1+2).
+    Local Notation "4" := (1+1+1+1).
+    Local Notation "9" := (3*3).
+    Local Notation "27" := (4*4 + 4+4 +1+1+1).
     Local Notation "'∞'" := unit : type_scope.
     Local Notation "'∞'" := (inr tt) : core_scope.
     Local Notation "( x , y )" := (inl (pair x y)).
     Local Open Scope core_scope.
 
-    Context {a b: F} {b_nonzero:b <> 0}.
-
-    Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
-    Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
-    Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
-    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
-    Local Notation Wopp := (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec).
+    Context {a b: F}
+            {aw bw}
+            {Haw : aw = (3-a^2)/(3*b^2)}
+            {Hbw : bw = (2*a^3-9*a)/(27*b^3)}.
 
     Ltac t :=
       repeat
@@ -61,23 +57,32 @@ Module M.
         | |- _ /\ _ => split | |- _ <-> _ => split
         end.
 
-    Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ :=
-      @Group.group_from_redundant_representation
-        Wpoint W.eq Wadd W.zero Wopp
-        (Algebra.Hierarchy.abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero)))
-        (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero))
-        (M.of_Weierstrass(b_nonzero:=b_nonzero))
-        (M.to_Weierstrass(b_nonzero:=b_nonzero))
-        _ _ _ _ _
-    .
-    Next Obligation. Proof. t; fsatz. Qed.
-    Next Obligation. Proof. t; fsatz. Qed.
-    Next Obligation. Proof. t; fsatz. Qed.
-    Next Obligation. Proof. t; fsatz. Qed.
-    Next Obligation. Proof. t; fsatz. Qed.
+    Global Instance MontgomeryWeierstrassIsomorphism {_1 _2 _3 _4 _5 _6 _7}
+           {discriminant_nonzero:id(4*aw*aw*aw + 27*bw*bw <> 0)}
+           {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}
+           {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28} (* XXX: this is a workaround for nsatz assuming arbitrary characteristic *)
+      :
+      @Group.isomorphic_commutative_groups
+        (@W.point F Feq Fadd Fmul aw bw)
+        W.eq
+        (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field _1 _2 aw bw)
+        W.zero
+        (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv aw bw field _1)
+
+        (@M.point F Feq Fadd Fmul a b)
+        M.eq
+        (M.add(char_ge_3:=_3)(b_nonzero:=_4))
+        M.zero
+        (M.opp(b_nonzero:=_7))
+        
+        (M.of_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_5))
+        (M.to_Weierstrass(Haw:=Haw)(Hbw:=Hbw)(b_nonzero:=_6)).
+    Proof.
+      eapply Group.commutative_group_by_isomorphism.
+      { eapply W.commutative_group; trivial. }
+      Time all:t.
+      Time par: abstract fsatz.
+    Qed.
 
-    Global Instance group discr_nonzero : Algebra.Hierarchy.group := proj1 (_MW discr_nonzero).
-    Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)).
-    Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)).
   End MontgomeryCurve.
 End M.
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
index 4c42d9464..be0153251 100644
--- a/src/Curves/Montgomery/XZProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -2,7 +2,11 @@ Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Tactics.SetoidSubst.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Curves.Montgomery.AffineInstances.
 Require Import Crypto.Curves.Montgomery.XZ BinPos.
 Require Import Coq.Classes.Morphisms.
 
@@ -11,7 +15,10 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
-            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}
+            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}
+            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}
+            {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -19,9 +26,6 @@ Module M.
     Local Notation "'∞'" := (inr tt) : core_scope.
     Local Notation "( x , y )" := (inl (pair x y)).
 
-    Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
-
     Context {a b: F} {b_nonzero:b <> 0}.
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
     Local Notation Madd := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
@@ -30,55 +34,214 @@ Module M.
     Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
     Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
 
+    Definition projective (P:F*F) :=
+      if dec (snd P = 0) then fst P <> 0 else True.
     Definition eq (P Q:F*F) := fst P * snd Q = fst Q * snd P.
 
-    Context {nonsquare_a24:forall r, r*r <> a*a - (1+1+1+1)}.
-    Let y_nonzero (Q:Mpoint) : match M.coordinates Q with ∞ => True | (x,y) => x <> 0 -> y <> 0 end.
-    Proof.
-      destruct Q as [Q pfQ]; destruct Q as [[x y]|[]]; cbv -[not]; intros; trivial.
-      specialize (nonsquare_a24 (x+x+a)); fsatz.
-    Qed.
+    Local Ltac do_unfold :=
+      cbv [eq projective fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep M.to_xz Let_In Proper respectful] in *.
 
-    Ltac t :=
-      repeat
-        match goal with
-        | _ => solve [ contradiction | trivial ]
-        | _ => progress intros
-        | _ => progress subst
-        | _ => progress Tactics.DestructHead.destruct_head' @M.point
-        | _ => progress Tactics.DestructHead.destruct_head' @prod
-        | _ => progress Tactics.DestructHead.destruct_head' @sum
-        | _ => progress Tactics.DestructHead.destruct_head' @and
-        | _ => progress Sum.inversion_sum
-        | _ => progress Prod.inversion_prod
-        | _ => progress Tactics.BreakMatch.break_match_hyps
-        | _ => progress Tactics.BreakMatch.break_match
-        | _ => progress cbv [eq fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep M.to_xz Let_In Proper respectful] in *
-        | |- _ /\ _ => split
-        end.
+    Ltac t_step _ :=
+      match goal with
+      | _ => solve [ contradiction | trivial ]
+      | _ => progress intros
+      | _ => progress subst
+      | _ => progress specialize_by_assumption
+      | [ H : ?x = ?x |- _ ] => clear H
+      | [ H : ?x <> ?x |- _ ] => specialize (H (reflexivity _))
+      | [ H0 : ?T, H1 : ~?T -> _ |- _ ] => clear H1
+      | _ => progress destruct_head'_prod
+      | _ => progress destruct_head'_and
+      | _ => progress Sum.inversion_sum
+      | _ => progress Prod.inversion_prod
+      | _ => progress cbv [fst snd proj1_sig projective eq] in * |-
+      | _ => progress cbn [to_xz M.coordinates proj1_sig] in * |-
+      | _ => progress destruct_head' @M.point
+      | _ => progress destruct_head'_sum
+      | [ H : context[dec ?T], H' : ~?T -> _ |- _ ]
+        => let H'' := fresh in
+           destruct (dec T) as [H''|H'']; [ clear H' | specialize (H' H'') ]
+      | _ => progress break_match_hyps
+      | _ => progress break_match
+      | |- _ /\ _ => split
+      | _ => progress do_unfold
+      end.
+    Ltac t := repeat t_step ().
 
+    (* happens if u=0 in montladder, all denominators remain 0 *)
+    Lemma add_0_numerator_r A B C D
+      :  snd (fst (xzladderstep 0 (pair C 0) (pair 0 A))) = 0
+      /\ snd (snd (xzladderstep 0 (pair D 0) (pair 0 B))) = 0.
+    Proof. t; fsatz. Qed.
     Lemma add_0_denominators A B C D
       :  snd (fst (xzladderstep 0 (pair A 0) (pair C 0))) = 0
       /\ snd (snd (xzladderstep 0 (pair B 0) (pair D 0))) = 0.
     Proof. t; fsatz. Qed.
 
-    Lemma add_0_numerator_l A B C D
-      :  snd (fst (xzladderstep 0 (pair 0 C) (pair A 0))) = 0
-      /\ snd (snd (xzladderstep 0 (pair 0 D) (pair B 0))) = 0.
-    Proof. t; fsatz. Qed.
+    (** This tactic is to work around deficiencies in the Coq 8.6
+        (released) version of [nsatz]; it has some heuristics for
+        clearing hypotheses and running [exfalso], and then tries to
+        solve the goal with [tac].  If [tac] fails on a goal, this
+        tactic does nothing. *)
+    Local Ltac exfalso_smart_clear_solve_by tac :=
+      try lazymatch goal with
+          | [ fld : Hierarchy.field (T:=?F) (eq:=?Feq), Feq_dec : DecidableRel ?Feq |- _ ]
+            => lazymatch goal with
+               | [ H : ?x * 1 = ?y * ?z, H' : ?x <> 0, H'' : ?z = 0 |- _ ]
+                 => clear -H H' H'' fld Feq_dec; exfalso; tac
+               | [ H : ?x * 0 = 1 * ?y, H' : ?y <> 0 |- _ ]
+                 => clear -H H' fld Feq_dec; exfalso; tac
+               | _
+                 => match goal with
+                    | [ H : ?b * ?lhs = ?rhs, H' : ?b * ?lhs' = ?rhs', Heq : ?x = ?y, Hb : ?b <> 0 |- _ ]
+                      => exfalso;
+                         repeat match goal with H : Ring.char_ge _ |- _ => revert H end;
+                         let rhs := match (eval pattern x in rhs) with ?f _ => f end in
+                         let rhs' := match (eval pattern y in rhs') with ?f _ => f end in
+                         unify rhs rhs';
+                         match goal with
+                         | [ H'' : ?x = ?Fopp ?x, H''' : ?x <> ?Fopp (?Fopp ?y) |- _ ]
+                           => let lhs := match (eval pattern x in lhs) with ?f _ => f end in
+                              let lhs' := match (eval pattern y in lhs') with ?f _ => f end in
+                              unify lhs lhs';
+                              clear -H H' Heq H'' H''' Hb fld Feq_dec; intros
+                         | [ H'' : ?x <> ?Fopp ?y, H''' : ?x <> ?Fopp (?Fopp ?y) |- _ ]
+                           => let lhs := match (eval pattern x in lhs) with ?f _ => f end in
+                              let lhs' := match (eval pattern y in lhs') with ?f _ => f end in
+                              unify lhs lhs';
+                              clear -H H' Heq H'' H''' Hb fld Feq_dec; intros
+                         end;
+                         tac
+                    | [ H : ?x * (?y * ?z) = 0 |- _ ]
+                      => exfalso;
+                         repeat match goal with
+                                | [ H : ?x * 1 = ?y * ?z |- _ ]
+                                  => is_var x; is_var y; is_var z;
+                                     revert H
+                                end;
+                         generalize fld;
+                         let lhs := match type of H with ?lhs = _ => lhs end in
+                         repeat match goal with
+                                | [ x : F |- _ ] => lazymatch type of H with
+                                                    | context[x] => fail
+                                                    | _ => clear dependent x
+                                                    end
+                                end;
+                         intros _; intros;
+                         tac
+                    end
+               end
+          end.
 
-    Lemma add_0_numerator_r A B C D
-      :  snd (fst (xzladderstep 0 (pair C 0) (pair 0 A))) = 0
-      /\ snd (snd (xzladderstep 0 (pair D 0) (pair 0 B))) = 0.
-    Proof. t; fsatz. Qed.
+    Lemma to_xz_add (x1:F) (xz x'z':F*F)
+          (Hxz:projective xz) (Hz'z':projective x'z')
+          (Q Q':Mpoint)
+          (HQ:eq xz (to_xz Q)) (HQ':eq x'z' (to_xz Q'))
+          (difference_correct:match M.coordinates (Madd Q (Mopp Q')) with
+                              | ∞ => False                  (* Q <> Q' *)
+                              | (x,y) => x = x1 /\ x1 <> 0  (* Q-Q' <> (0, 0) *)
+                              end)
+      :  eq (to_xz (Madd Q Q )) (fst (xzladderstep x1 xz xz))
+      /\ eq (to_xz (Madd Q Q')) (snd (xzladderstep x1 xz x'z'))
+      /\ projective (snd (xzladderstep x1 xz x'z')).
+    Proof.
+      fsatz_prepare_hyps.
+      Time t.
+      Time par: abstract (exfalso_smart_clear_solve_by fsatz || fsatz).
+    Time Qed.
+
+    Context {a2m4_nonsquare:forall r, r*r <> a*a - (1+1+1+1)}.
+
+    Lemma projective_fst_xzladderstep x1 Q (HQ:projective Q)
+      :  projective (fst (xzladderstep x1 Q Q)).
+    Proof.
+      specialize (a2m4_nonsquare (fst Q/snd Q  - fst Q/snd Q)).
+      destruct (dec (snd Q = 0)); t; specialize_by assumption; fsatz.
+    Qed.
+
+    Let a2m4_nz : a*a - (1+1+1+1) <> 0.
+    Proof. specialize (a2m4_nonsquare 0). fsatz. Qed.
+
+    Lemma difference_preserved Q Q' :
+          M.eq
+            (Madd (Madd Q Q) (Mopp (Madd Q Q')))
+            (Madd Q (Mopp Q')).
+    Proof.
+      pose proof (let (_, h, _, _) := AffineInstances.M.MontgomeryWeierstrassIsomorphism b_nonzero (a:=a) a2m4_nz in h) as commutative_group.
+      rewrite Group.inv_op.
+      rewrite <-Hierarchy.associative.
+      rewrite Group.cancel_left.
+      rewrite Hierarchy.commutative.
+      rewrite <-Hierarchy.associative.
+      rewrite Hierarchy.left_inverse.
+      rewrite Hierarchy.right_identity.
+      reflexivity.
+    Qed.
 
-    Lemma to_xz_add (x1:F) (Q Q':Mpoint)
+    Lemma to_xz_add'
+          (x1:F)
+          (xz x'z':F*F)
+          (Q Q':Mpoint)
+
+          (HQ:eq xz (to_xz Q))
+          (HQ':eq x'z' (to_xz Q'))
+          (Hxz:projective xz)
+          (Hx'z':projective x'z')
           (difference_correct:match M.coordinates (Madd Q (Mopp Q')) with
                               | ∞ => False                  (* Q <> Q' *)
                               | (x,y) => x = x1 /\ x1 <> 0  (* Q-Q' <> (0, 0) *)
                               end)
-      :  eq (to_xz (Madd Q Q )) (fst (xzladderstep x1 (to_xz Q) (to_xz Q )))
-      /\ eq (to_xz (Madd Q Q')) (snd (xzladderstep x1 (to_xz Q) (to_xz Q'))).
-    Proof. specialize (y_nonzero Q); t; fsatz. Qed.
+      :
+           eq (to_xz (Madd Q Q )) (fst (xzladderstep x1 xz xz))
+        /\ eq (to_xz (Madd Q Q')) (snd (xzladderstep x1 xz x'z'))
+        /\ projective (fst (xzladderstep x1 xz x'z'))
+        /\ projective (snd (xzladderstep x1 xz x'z'))
+        /\ match M.coordinates (Madd (Madd Q Q) (Mopp (Madd Q Q'))) with
+                              | ∞ => False                  (* Q <> Q' *)
+                              | (x,y) => x = x1 /\ x1 <> 0  (* Q-Q' <> (0, 0) *)
+                              end.
+    Proof.
+      destruct (to_xz_add x1 xz x'z' Hxz Hx'z' Q Q' HQ HQ' difference_correct) as [? [? ?]].
+      split; [|split; [|split;[|split]]]; eauto.
+      {
+        pose proof projective_fst_xzladderstep x1 xz Hxz.
+        destruct_head prod.
+        cbv [projective fst xzladderstep] in *; eauto. }
+      {
+        pose proof difference_preserved Q Q' as HQQ;
+        destruct (Madd (Madd Q Q) (Mopp (Madd Q Q'))) as [[[xQ yQ]|[]]pfQ];
+        destruct (Madd Q (Mopp Q')) as [[[xD yD]|[]]pfD];
+        cbv [M.coordinates proj1_sig M.eq] in *;
+        destruct_head' and; try split;
+          try contradiction; try etransitivity; eauto.
+      }
+    Qed.
+
+    Definition to_x (xz:F*F) : F :=
+      if dec (snd xz = 0) then 0 else fst xz / snd xz.
+
+    Lemma to_x_to_xz Q : to_x (to_xz Q) = match M.coordinates Q with
+                                          | ∞ => 0
+                                          | (x,y) => x
+                                          end.
+    Proof.
+      cbv [to_x]; t; fsatz.
+    Qed.
+
+    Lemma proper_to_x_projective xz x'z'
+           (Hxz:projective xz) (Hx'z':projective x'z')
+           (H:eq xz x'z') : Feq (to_x xz) (to_x x'z').
+    Proof.
+      destruct (dec (snd xz = 0)), (dec(snd x'z' = 0));
+        cbv [to_x]; t;
+        specialize_by (assumption||reflexivity);
+        try fsatz.
+    Qed.
+
+    Lemma to_x_zero x : to_x (pair x 0) = 0.
+    Proof. cbv; t; fsatz. Qed.
+
+    Lemma projective_to_xz Q : projective (to_xz Q).
+    Proof. t; fsatz. Qed.
   End MontgomeryCurve.
 End M.
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v
index be76cee90..3401d7b31 100644
--- a/src/Curves/Weierstrass/AffineProofs.v
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -9,10 +9,7 @@ Module W.
   Section W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {Feq_dec:DecidableRel Feq}
-            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *)
-    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+            {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "-" := Fsub. Local Infix "*" := Fmul.
@@ -24,7 +21,7 @@ Module W.
              | |- Equivalence _ => split; [intros ? | intros ??? | intros ????? ]
              | |- monoid => split
              | |- group => split
-             | |- abelian_group => split
+             | |- commutative_group => split
              | |- is_associative => split; intros ???
              | |- is_commutative => split; intros ??
              | |- is_left_inverse => split; intros ?
@@ -33,8 +30,12 @@ Module W.
              | |- is_right_identity => split; intros ?
              end.
 
-    Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
-    Proof using Type.
+    Global Instance commutative_group
+           char_ge_3
+           {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *)
+           {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)}
+      : commutative_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
+    Proof using Type. 
       Time
         cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig];
           repeat match goal with