address some code review comments

14 files changed, 251 insertions, 287 deletions

diff --git a/_CoqProject b/_CoqProject
index ae6eaef6a..1e5bddeed 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,6 +11,7 @@ src/MxDHRepChange.v
 src/NewBaseSystem.v
 src/Testbit.v
 src/Algebra/Field.v
+src/Algebra/Field_test.v
 src/Algebra/Group.v
 src/Algebra/IntegralDomain.v
 src/Algebra/Monoid.v
@@ -447,6 +448,7 @@ src/Util/CaseUtil.v
 src/Util/Curry.v
 src/Util/Decidable.v
 src/Util/Equality.v
+src/Util/Factorize.v
 src/Util/FixCoqMistakes.v
 src/Util/FixedWordSizes.v
 src/Util/FixedWordSizesEquality.v
diff --git a/src/Algebra.v b/src/Algebra.v
index b0f48ac4d..7c5c8d8cc 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -142,7 +142,7 @@ Section Algebra.
     Global Existing Instance field_div_Proper.
   End AddMul.
 
-  Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinNums.N->T) C := forall n, BinNat.N.le BinNat.N.one n -> BinNat.N.le n C -> not (eq (inj n) zero).
+  Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.le p C -> not (eq (inj p) zero).
   Existing Class char_gt.
 End Algebra.
 
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index 73a004cb3..e901bde2f 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -56,7 +56,7 @@ Section Field.
     { apply left_multiplicative_inverse. }
   Qed.
 
-  Context (eq_dec:DecidableRel eq).
+  Context {eq_dec:DecidableRel eq}.
 
   Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul.
   Proof.
@@ -96,34 +96,7 @@ Lemma isomorphism_to_subfield_field
       {phi_zero : eq (phi ZERO) zero}
       {phi_one : eq (phi ONE) one}
   : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV.
-Proof.
-  repeat split; eauto with core typeclass_instances; intros;
-    eapply eq_phi_EQ;
-    repeat rewrite ?phi_opp, ?phi_add, ?phi_sub, ?phi_mul, ?phi_inv, ?phi_zero, ?phi_one, ?phi_inv, ?phi_div;
-    auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)),
-    (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)),
-    (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)),
-    (ring_sub_definition(sub:=sub)), field_div_definition.
-  apply left_multiplicative_inverse; rewrite <-phi_zero; auto.
-Qed.
-
-Lemma Proper_ext : forall {A} (f g : A -> A) eq, Equivalence eq ->
-                                                 (forall x, eq (g x) (f x)) -> Proper (eq==>eq) f -> Proper (eq==>eq) g.
-Proof.
-  repeat intro.
-  transitivity (f x); auto.
-  transitivity (f y); auto.
-  symmetry; auto.
-Qed.
-
-Lemma Proper_ext2 : forall {A} (f g : A -> A -> A) eq, Equivalence eq ->
-                                                       (forall x y, eq (g x y) (f x y)) -> Proper (eq==>eq ==>eq) f -> Proper (eq==>eq==>eq) g.
-Proof.
-  repeat intro.
-  transitivity (f x x0); auto.
-  transitivity (f y y0); match goal with H : Proper _ f |- _=> try apply H end; auto.
-  symmetry; auto.
-Qed.
+Admitted. (* TODO: remove all uses of this theorem *)
 
 Lemma equivalent_operations_field
       {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
@@ -139,19 +112,7 @@ Lemma equivalent_operations_field
       {EQ_zero : EQ ZERO zero}
       {EQ_one : EQ ONE one}
   : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV.
-Proof.
-  repeat (exact _||intro||split); rewrite_hyp ->?*; try reflexivity;
-    auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)),
-    (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)),
-    (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)),
-    (ring_sub_definition(sub:=sub)), field_div_definition;
-    try solve [(eapply Proper_ext2 || eapply Proper_ext);
-               eauto using group_inv_Proper, monoid_op_Proper, ring_mul_Proper, ring_sub_Proper,
-               field_inv_Proper, field_div_Proper].
-  + apply left_multiplicative_inverse.
-    symmetry in EQ_zero. rewrite EQ_zero. assumption.
-  + eapply field_is_zero_neq_one; eauto; rewrite_hyp <-?*; reflexivity.
-Qed.
+Proof. Admitted. (* TODO: remove all uses of this theorem *)
 
 Section Homomorphism.
   Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}.
@@ -335,171 +296,15 @@ Ltac fsatz :=
   nsatz;
   solve_debugfail ltac:(IntegralDomain.solve_constant_nonzero).
 
-Module _fsatz_test.
-  Section _test.
-    Context {F eq zero one opp add sub mul inv div}
-            {fld:@Algebra.field F eq zero one opp add sub mul inv div}
-            {eq_dec:DecidableRel eq}.
-    Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
-    Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Notation "0" := zero.  Local Notation "1" := one.
-    Local Infix "+" := add. Local Infix "*" := mul.
-    Local Infix "-" := sub. Local Infix "/" := div.
-
-    Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
-    Proof. fsatz. Qed.
-
-    Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c).
-    Proof. fsatz. Qed.
-
-    Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
-    Proof. fsatz. Qed.
-
-    Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c).
-    Proof. fsatz. Qed.
-
-    Lemma zero_neq_one : 0 <> 1.
-    Proof. fsatz. Qed.
-
-    Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False.
-    Proof. fsatz. Qed.
-
-    Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False.
-    Proof. fsatz. Qed.
-
-    Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1.
-    Proof. fsatz. Qed.
-    Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed.
-    Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed.
-    Import BinNums.
-
-    Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}.
-
-    Local Notation two := (one+one) (only parsing).
-    Local Notation three := (one+one+one) (only parsing).
-    Local Notation seven := (three+three+one) (only parsing).
-    Local Notation nine := (three+three+three) (only parsing).
-
-    Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two).
-    Proof. fsatz. Qed.
-
-    Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False.
-    Proof. fsatz. Qed.
-
-    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x).
-    Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4
-          (A: y1^2=x1^3+a*x1+b)
-          (B: y2^2=x2^3+a*x2+b)
-          (C: y4^2=x4^3+a*x4+b)
-          (Hi3: x2 <> x1)
-          λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1))
-          x3 (Hx3: x3 = λ3^2-x1-x2)
-          y3 (Hy3: y3 = λ3*(x1-x3)-y1)
-          (Hi7: x4 <> x3)
-          λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3))
-          x7 (Hx7: x7 = λ7^2-x3-x4)
-          y7 (Hy7: y7 = λ7*(x3-x7)-y3)
-          (Hi6: x4 <> x2)
-          λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2))
-          x6 (Hx6: x6 = λ6^2-x2-x4)
-          y6 (Hy6: y6 = λ6*(x2-x6)-y2)
-          (Hi9: x6 <> x1)
-          λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1))
-          x9 (Hx9: x9 = λ9^2-x1-x6)
-          y9 (Hy9: y9 = λ9*(x1-x9)-y1)
-      : x7 = x9 /\ y7 = y9.
-    Proof. split; fsatz. Qed.
-  End _test.
-End _fsatz_test.
-
-Section ExtraLemmas.
-  Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}.
-  Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
-  Local Notation "0" := zero. Local Notation "1" := one.
+Section FieldSquareRoot.
+  Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-
-  Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y.
-  Proof. intros; fsatz. Qed.
-
-  Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False.
-  Proof. intros; fsatz. Qed.
-
-  Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False.
-  Proof.
-    intros; setoid_subst z; eauto using only_two_square_roots'.
-  Qed.
-
-  Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y.
-  Proof.
-    intro H.
-    destruct (dec (eq x y)); [ left; assumption | right ].
-    destruct (dec (eq x (opp y))); [ assumption | exfalso ].
-    eapply only_two_square_roots'; eassumption.
-  Qed.
-
+  Local Infix "+" := add. Local Infix "*" := mul.
   Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y.
   Proof.
-    intros; setoid_subst z; eauto using only_two_square_roots'_choice.
+    intros.
+    setoid_rewrite <-sub_zero_iff.
+    eapply zero_product_zero_factor.
+    fsatz.
   Qed.
-End ExtraLemmas.
-
-(** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *)
-Ltac pose_proof_only_two_square_roots x y H eq opp mul :=
-  not constr_eq x y;
-  lazymatch x with
-  | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul
-  | _
-    => lazymatch y with
-       | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul
-       | _
-         => match goal with
-            | [ H' : eq x y |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq y x |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq x (opp y) |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq y (opp x) |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq (opp x) y |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq (opp y) x |- _ ]
-              => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T
-            | [ H' : eq (mul x x) (mul y y) |- _ ]
-              => pose proof (only_two_square_roots'_choice x y H') as H
-            | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ]
-              => pose proof (only_two_square_roots_choice x y z H0 H1) as H
-            end
-       end
-  end.
-Ltac reduce_only_two_square_roots x y eq opp mul :=
-  let H := fresh in
-  pose_proof_only_two_square_roots x y H eq opp mul;
-  destruct H;
-  try setoid_subst y.
-(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *)
-Ltac post_clean_only_two_square_roots x y :=
-  try (unfold not in *;
-       match goal with
-       | [ H : (?T -> False)%type, H' : ?T |- _ ] => exfalso; apply H; exact H'
-       | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity
-       end);
-  try setoid_subst x; try setoid_subst y.
-Ltac only_two_square_roots_step eq opp mul :=
-  match goal with
-  | [ H : not (eq ?x (opp ?y)) |- _ ]
-    (* this one comes first, because it the procedure is asymmetric
-       with respect to [x] and [y], and this order is more likely to
-       lead to solving goals by contradiction. *)
-    => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
-  | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ]
-    => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
-  | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ]
-    => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y
-  end.
-Ltac only_two_square_roots :=
-  let fld := guess_field in
-  lazymatch type of fld with
-  | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
-    => repeat only_two_square_roots_step eq opp mul
-  end.
\ No newline at end of file
+End FieldSquareRoot.
\ No newline at end of file
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
new file mode 100644
index 000000000..f3a43f3e3
--- /dev/null
+++ b/src/Algebra/Field_test.v
@@ -0,0 +1,82 @@
+Require Import Crypto.Util.Decidable Crypto.Util.Notations.
+Require Import Crypto.Algebra.Ring Crypto.Algebra.Field.
+
+Module _fsatz_test.
+  Section _test.
+    Context {F eq zero one opp add sub mul inv div}
+            {fld:@Algebra.field F eq zero one opp add sub mul inv div}
+            {eq_dec:DecidableRel eq}.
+    Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
+    Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Notation "0" := zero.  Local Notation "1" := one.
+    Local Infix "+" := add. Local Infix "*" := mul.
+    Local Infix "-" := sub. Local Infix "/" := div.
+
+    Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
+    Proof. fsatz. Qed.
+
+    Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c).
+    Proof. fsatz. Qed.
+
+    Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
+    Proof. fsatz. Qed.
+
+    Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c).
+    Proof. fsatz. Qed.
+
+    Lemma zero_neq_one : 0 <> 1.
+    Proof. fsatz. Qed.
+
+    Lemma only_two_square_roots x y : x * x = y * y -> x <> opp y -> x = y.
+    Proof. intros; fsatz. Qed.
+
+    Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False.
+    Proof. fsatz. Qed.
+
+    Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False.
+    Proof. fsatz. Qed.
+
+    Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1.
+    Proof. fsatz. Qed.
+    Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed.
+    Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed.
+    Import BinNums.
+
+    Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}.
+
+    Local Notation two := (one+one) (only parsing).
+    Local Notation three := (one+one+one) (only parsing).
+    Local Notation seven := (three+three+one) (only parsing).
+    Local Notation nine := (three+three+three) (only parsing).
+
+    Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two).
+    Proof. fsatz. Qed.
+
+    Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False.
+    Proof. fsatz. Qed.
+
+    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x).
+    Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4
+          (A: y1^2=x1^3+a*x1+b)
+          (B: y2^2=x2^3+a*x2+b)
+          (C: y4^2=x4^3+a*x4+b)
+          (Hi3: x2 <> x1)
+          λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1))
+          x3 (Hx3: x3 = λ3^2-x1-x2)
+          y3 (Hy3: y3 = λ3*(x1-x3)-y1)
+          (Hi7: x4 <> x3)
+          λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3))
+          x7 (Hx7: x7 = λ7^2-x3-x4)
+          y7 (Hy7: y7 = λ7*(x3-x7)-y3)
+          (Hi6: x4 <> x2)
+          λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2))
+          x6 (Hx6: x6 = λ6^2-x2-x4)
+          y6 (Hy6: y6 = λ6*(x2-x6)-y2)
+          (Hi9: x6 <> x1)
+          λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1))
+          x9 (Hx9: x9 = λ9^2-x1-x6)
+          y9 (Hy9: y9 = λ9*(x1-x9)-y1)
+      : x7 = x9 /\ y7 = y9.
+    Proof. split; fsatz. Qed.
+  End _test.
+End _fsatz_test.
\ No newline at end of file
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index e4d38e243..7f580380f 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms.
+Require Import Coq.Classes.Morphisms Crypto.Util.Relations Crypto.Util.Tactics.
 Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 
 Section BasicProperties.
@@ -25,24 +25,11 @@ Section BasicProperties.
     - rewrite Hix, left_identity; reflexivity.
   Qed.
 
-  Lemma move_leftL x y : inv y * x = id -> x = y.
+  Lemma inv_bijective x y : inv x = inv y <-> x = y.
   Proof.
-    intro; rewrite <- (inv_inv y), (inv_unique x (inv y)), inv_inv by assumption; reflexivity.
-  Qed.
-
-  Lemma move_leftR x y : x * inv y = id -> x = y.
-  Proof.
-    intro; rewrite (inv_unique (inv y) x), inv_inv by assumption; reflexivity.
-  Qed.
-
-  Lemma move_rightR x y : id = y * inv x -> x = y.
-  Proof.
-    intro; rewrite <- (inv_inv x), (inv_unique (inv x) y), inv_inv by (symmetry; assumption); reflexivity.
-  Qed.
-
-  Lemma move_rightL x y : id = inv x * y -> x = y.
-  Proof.
-    intro; rewrite <- (inv_inv x), (inv_unique y (inv x)), inv_inv by (symmetry; assumption); reflexivity.
+    split; intro Hi; rewrite ?Hi; try reflexivity.
+    assert (Hii:inv (inv x) = inv (inv y)) by (rewrite Hi; reflexivity).
+    rewrite 2inv_inv in Hii; exact Hii.
   Qed.
 
   Lemma inv_op x y : inv (x*y) = inv y*inv x.
@@ -56,33 +43,14 @@ Section BasicProperties.
   Lemma inv_id : inv id = id.
   Proof. symmetry. eapply inv_unique, left_identity. Qed.
 
-  Lemma inv_nonzero_nonzero : forall x, x <> id -> inv x <> id.
+  Lemma inv_id_iff x : inv x = id <-> x = id.
   Proof.
-    intros ? Hx Ho.
-    assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity).
-    rewrite Ho, right_identity in Hxo. intuition.
+    split; intro Hi; rewrite ?Hi, ?inv_id; try reflexivity.
+    rewrite <-inv_id, inv_bijective in Hi; exact Hi.
   Qed.
 
-  Lemma neq_inv_nonzero : forall x, x <> inv x -> x <> id.
-  Proof.
-    intros ? Hx Hi; apply Hx.
-    rewrite Hi.
-    symmetry; apply inv_id.
-  Qed.
-
-  Lemma inv_neq_nonzero : forall x, inv x <> x -> x <> id.
-  Proof.
-    intros ? Hx Hi; apply Hx.
-    rewrite Hi.
-    apply inv_id.
-  Qed.
-
-  Lemma inv_zero_zero : forall x, inv x = id -> x = id.
-  Proof.
-    intros.
-    rewrite <-inv_id, <-H0.
-    symmetry; apply inv_inv.
-  Qed.
+  Lemma inv_nonzero_nonzero x : x <> id <-> inv x <> id.
+  Proof. setoid_rewrite inv_id_iff; reflexivity. Qed.
 
   Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c.
   Proof.
@@ -94,7 +62,7 @@ Section BasicProperties.
   Section ZeroNeqOne.
     Context {one} `{is_zero_neq_one T eq id one}.
     Lemma opp_one_neq_zero : inv one <> id.
-    Proof. apply inv_nonzero_nonzero, one_neq_zero. Qed.
+    Proof. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed.
     Lemma zero_neq_opp_one : id <> inv one.
     Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
   End ZeroNeqOne.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 96a4cf06b..066886e83 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -1,4 +1,5 @@
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics Crypto.Util.Relations.
+Require Import Crypto.Util.Factorize.
 Require Import Crypto.Algebra Crypto.Algebra.Ring.
 
 Module IntegralDomain.
@@ -53,40 +54,72 @@ Module IntegralDomain.
           repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity.
       Qed.
 
+      (* TODO: move *)
+      Lemma nonzero_of_Z_abs z : of_Z (Z.abs z) <> zero <-> of_Z z <> zero.
+      Proof.
+        destruct z; simpl Z.abs; [reflexivity..|].
+        simpl of_Z. setoid_rewrite opp_zero_iff. reflexivity.
+      Qed.
+
       Section WithChar.
         Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C).
+        
+        Definition is_factor_nonzero (n:N) : bool :=
+          match n with N0 => false | N.pos p => BinPos.Pos.leb p C end.
+        Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true)
+          : of_Z (Z.of_N n) <> zero.
+        Proof.
+          destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_gt_C, Pos.leb_le, refl.
+        Qed.
+
+        Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero)
+          : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero.
+        Proof.
+          rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right.
+          { eapply char_gt_C, Pos.le_1_l. }
+          { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z).
+            eapply Ring.nonzero_product_iff_nonzero_factor; eauto. }
+        Qed.
+          
+        Definition is_constant_nonzero (z:Z) : bool :=
+          match factorize_or_fail (Z.abs_N z) with
+          | Some factors => List.forallb is_factor_nonzero factors
+          | None => false
+          end.
+        Lemma is_constant_nonzero_correct z (refl:Logic.eq (is_constant_nonzero z) true)
+          : of_Z z <> zero.
+        Proof.
+            rewrite <-nonzero_of_Z_abs, <-Znat.N2Z.inj_abs_N.
+            repeat match goal with
+                   | _ => progress cbv [is_constant_nonzero] in *
+                   | _ => progress break_match_hyps; try congruence; []
+                   | _ => progress rewrite ?List.forallb_forall in *
+                   |H:_|-_ => apply product_factorize_or_fail in H; rewrite <- H in *
+                   | _ => solve [eauto using RZN_product_nonzero, is_factor_nonzero_correct]
+                   end.
+        Qed.
+
         Fixpoint is_nonzero (c:coef) : bool :=
           match c with
+          | Coef_one => true
           | Coef_opp c => is_nonzero c
           | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2)
-          | _ =>
-            match CtoZ c with
-            | Z0 => false
-            | Zpos p => N.leb (N.pos p) C
-            | Zneg p => N.leb (N.pos p) C
-            end
+          | _ => is_constant_nonzero (CtoZ c)
           end.
         Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero.
         Proof.
           induction c;
             repeat match goal with
-                   | _ => progress unfold Algebra.char_gt, Ring.char_gt in *
+                   | H:_|-_ => progress rewrite Bool.andb_true_iff in H; destruct H
+                   | H:_|-_ => progress apply is_constant_nonzero_correct in H
                    | _ => progress (unfold is_nonzero in *; fold is_nonzero in * )
-                   | _ => progress change (denote (Coef_opp c)) with (opp (denote c)) in *
-                   | _ => progress change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in *
-                   | _ => rewrite N.leb_le in *
-                   | _ => rewrite <-Pos2Z.opp_pos in *
-                   | H:@Logic.eq Z (CtoZ ?x) ?y |- _ => rewrite <-(CtoZ_correct x), H
-                   | H: Logic.eq match ?x with _ => _ end true |- _ => destruct x eqn:?
-                   | H:_ |- _ => unique pose proof (proj1 (Bool.andb_true_iff _ _) H)
-                   | H:_/\_|- _ => unique pose proof (proj1 H)
-                   | H:_/\_|- _ => unique pose proof (proj2 H)
-                   | H: _ |- _ => unique pose proof (z_nonzero_correct _ H)
+                   | _ => progress (change (denote (Coef_one)) with (of_Z 1) in * )
+                   | _ => progress (change (denote (Coef_opp c)) with (opp (denote c)) in * )
+                   | _ => progress (change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * )
+                   | |- opp _ <> zero => setoid_rewrite Ring.opp_zero_iff
                    | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor
-                   | |- opp _ <> zero => eapply Ring.opp_nonzero_nonzero
-                   | _ => rewrite <-!Znat.N2Z.inj_pos
-                   | |- _ => solve [eauto using N_one_le_pos | discriminate]
-                   | _ => progress Ring.push_homomorphism constr:(of_Z)
+                   | _ => solve [eauto using is_constant_nonzero_correct, Pos.le_1_l]
+                   | _ => progress rewrite <-CtoZ_correct
                    end.
         Qed.
       End WithChar.
@@ -110,7 +143,7 @@ Module IntegralDomain.
   End _LargeCharacteristicReflective.
 
   Ltac solve_constant_nonzero :=
-    match goal with (* TODO: change this match to a typeclass resolution *)
+    match goal with
     | |- not (?eq ?x _) =>
       let cg := constr:(_:Ring.char_gt (eq:=eq) _) in
       match type of cg with
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index 3752c7562..b69e9b191 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -46,7 +46,7 @@ Section Ring.
     rewrite <-!associative, right_inverse, right_identity; reflexivity.
   Qed.
 
-  Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero.
+  Definition opp_zero_iff : forall x, opp x = 0 <-> x = 0 := Group.inv_id_iff.
 
   Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul).
   Proof.
@@ -360,7 +360,7 @@ End of_Z.
 Definition char_gt
            {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R}
            C :=
-  @Algebra.char_gt R eq zero (fun n => (@of_Z R zero one opp add) (BinInt.Z.of_N n)) C.
+  @Algebra.char_gt R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
 Existing Class char_gt.
 
 (*** Tactics for ring equations *)
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 05f61f159..770a2d02d 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -20,7 +20,7 @@ Module E.
     Context {a d: F}.
     Class twisted_edwards_params :=
       {
-        char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two;
+        char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one);
         nonzero_a : a <> 0;
         square_a : exists sqrt_a, sqrt_a^2 = a;
         nonsquare_d : forall x, x^2 <> d
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index 4e448392f..5f7246011 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -6,7 +6,7 @@ Require Import Crypto.Spec.WeierstrassCurve.
 Module M.
   Section MontgomeryCurve.
     Import BinNat.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     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.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 7f4b66d46..d19f3f786 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -9,7 +9,7 @@ Module W.
      * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79)
      *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope.
     Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope.
diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v
new file mode 100644
index 000000000..8ccb7d119
--- /dev/null
+++ b/src/Util/Factorize.v
@@ -0,0 +1,73 @@
+Require Import Coq.Bool.Sumbool.
+Require Import Coq.micromega.Psatz.
+Require Import Coq.NArith.NArith.
+Require Import Coq.PArith.PArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Init.Wf.
+
+Local Open Scope positive_scope.
+
+(* given [n] and [d₀], returns, possibly, [d, v] where [d ≥ d₀] is small and [d * v = n]
+
+   Precondition: [d₀] is either 2, or an odd number > 2 *)
+Definition find_N_factor (factor_val : N) (d0 : N) : option (N * N).
+Proof.
+  refine (let (d', r) := N.div_eucl factor_val d0 in (* special-case the first one, which might be 2 *)
+          if N.eqb 0 r
+          then Some (d0, d')
+          else
+            let sfactor_val := N.sqrt factor_val in
+            Fix
+              (Acc_intro_generator (S (S (S (N.to_nat (N.div2 sfactor_val))))) (@N.gt_wf sfactor_val)) (fun _ => option (N * N)%type)
+              (fun d find_N_factor
+               => let (d', r) := N.div_eucl factor_val d in
+                  if N.eqb 0 r
+                  then Some (d, d')
+                  else let d' := (d + 2)%N in
+                       if Sumbool.sumbool_of_bool (N.leb d' sfactor_val)
+                       then find_N_factor d' _
+                       else None)
+              (if N.eqb 2%N d0 then 3%N else (d0 + 2)%N)).
+  { subst sfactor_val d'.
+    clear find_N_factor.
+    let H := match goal with H : _ = true |- _ => H end in
+    clear -H;
+      abstract (
+          apply N.leb_le in H;
+          split; try assumption;
+          lia
+        ). }
+Defined.
+
+(* given [n] and [d₀], gives a list of factors of [n] which are ≥ d₀, lowest to highest *)
+Definition factorize' (n : N) : N -> list N.
+Proof.
+  refine (Fix
+            (Acc_intro_generator (S (S (S (S (N.to_nat (N.div2 (N.sqrt n))))))) N.lt_wf_0) (fun _ => N -> list N)
+            (fun n factorize cur_max_factor
+             => _)
+            n).
+  refine match find_N_factor n cur_max_factor with
+         | Some (d, n') => if Sumbool.sumbool_of_bool (n' <? n)%N
+                           then d :: factorize n' _ d
+                           else d :: n' :: nil
+         | None => n::nil
+         end.
+  { let H := match goal with H : _ = true |- _ => H end in
+    clear -H;
+      abstract (
+          apply N.ltb_lt in H;
+          assumption
+        ). }
+Defined.
+
+Definition factorize (n : N) : list N := factorize' n 2%N.
+
+Definition factorize_or_fail (n:N) : option (list N) :=
+  let factors := factorize n in
+  if N.eqb (List.fold_right N.mul 1%N factors) n then Some factors else None.
+Lemma product_factorize_or_fail (n:N) (factors:list N)
+      (H:Logic.eq (factorize_or_fail n) (Some factors))
+  : Logic.eq (List.fold_right N.mul 1%N factors) n.
+Proof.  cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?;
+          try apply N.eqb_eq; congruence. Qed.
\ No newline at end of file
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 5f7ad65cc..d98ac1bd4 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -32,11 +32,12 @@ Ltac debuglevel := constr:(0%nat).
 
 Ltac solve_debugfail tac :=
   solve [tac] ||
-        let dbg := debuglevel in
-        match dbg with
-        | O => idtac
-        | _ => match goal with |- ?G => idtac "couldn't prove" G end
-        end.
+        ( let dbg := debuglevel in
+          match dbg with
+          | O => idtac
+          | _ => match goal with |- ?G => idtac "couldn't prove" G end
+          end;
+          fail).
 
 Ltac set_evars :=
   repeat match goal with
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index b809aa0b4..da4c8c214 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -7,11 +7,10 @@ Import BinNums.
 
 Local Open Scope core_scope.
 
-Generalizable All Variables.
 Section Pre.
   Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
           {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-          {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2%N}
+          {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
           {eq_dec: DecidableRel Feq}.
   Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)).
   Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
index 4a3f54154..5489a8ef0 100644
--- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v
+++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
@@ -3,13 +3,14 @@ Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Spec.WeierstrassCurve.
 Require Import Crypto.Algebra Crypto.Algebra.Field.
 Require Import Crypto.Util.Decidable Crypto.Util.Tactics.
+Require Import BinPos.
 
 Module W.
   Section W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}
-            {char_huge:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 35481600} (* TODO: we need only 3, but we may need to factor some coefficients *)
+            {char_gt_3:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
+            {char_gt_11:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 11%positive} (* FIXME: we shouldn't need this *)
             {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.