split the algebra library; use fsatz more

7 files changed, 1402 insertions, 150 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
new file mode 100644
index 000000000..ddd2737a3
--- /dev/null
+++ b/src/Algebra/Field.v
@@ -0,0 +1,481 @@
+Require Import Crypto.Util.Relations Crypto.Util.Tactics.
+Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
+Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
+Require Coq.setoid_ring.Field_theory.
+
+Section Field.
+  Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div}.
+  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.
+
+  Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one.
+  Proof.
+    intros. rewrite commutative. auto using left_multiplicative_inverse.
+  Qed.
+
+  Lemma left_inv_unique x ix : ix * x = one -> ix = inv x.
+  Proof.
+    intro Hix.
+    assert (ix*x*inv x = inv x).
+    - rewrite Hix, left_identity; reflexivity.
+    - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial.
+      intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix.
+      apply (zero_neq_one(eq:=eq)). assumption.
+  Qed.
+  Definition inv_unique := left_inv_unique.
+
+  Lemma right_inv_unique x ix : x * ix = one -> ix = inv x.
+  Proof. rewrite commutative. apply left_inv_unique. Qed.
+
+  Lemma div_one x : div x one = x.
+  Proof.
+    rewrite field_div_definition.
+    rewrite <-(inv_unique 1 1); apply monoid_is_right_identity.
+  Qed.
+
+  Lemma mul_cancel_l_iff : forall x y, y <> 0 ->
+                                       (x * y = y <-> x = one).
+  Proof.
+    intros.
+    split; intros.
+    + rewrite <-(right_multiplicative_inverse y) by assumption.
+      rewrite <-H1 at 1; rewrite <-associative.
+      rewrite right_multiplicative_inverse by assumption.
+      rewrite right_identity.
+      reflexivity.
+    + rewrite H1; apply left_identity.
+  Qed.
+
+  Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq.
+  Proof.
+    constructor.
+    { apply Ring.ring_theory_for_stdlib_tactic. }
+    { intro H01. symmetry in H01. auto using (zero_neq_one(eq:=eq)). }
+    { apply field_div_definition. }
+    { apply left_multiplicative_inverse. }
+  Qed.
+
+  Context (eq_dec:DecidableRel eq).
+
+  Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul.
+  Proof.
+    split. intros x y Hxy.
+    eapply not_not; try typeclasses eauto; []; intuition idtac; eapply (zero_neq_one(eq:=eq)).
+    transitivity ((inv y * (inv x * x)) * y).
+    - rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity.
+    - rewrite left_multiplicative_inverse, right_identity, left_multiplicative_inverse by trivial.
+      reflexivity.
+  Qed.
+
+  Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
+  Proof.
+    split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
+  Qed.
+End Field.
+
+Lemma isomorphism_to_subfield_field
+      {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
+      {Equivalence_EQ: @Equivalence T EQ}
+      {Proper_OPP:Proper(EQ==>EQ)OPP}
+      {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
+      {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
+      {Proper_MUL:Proper(EQ==>EQ==>EQ)MUL}
+      {Proper_INV:Proper(EQ==>EQ)INV}
+      {Proper_DIV:Proper(EQ==>EQ==>EQ)DIV}
+      {R eq zero one opp add sub mul inv div} {fieldR:@field R eq zero one opp add sub mul inv div}
+      {phi}
+      {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
+      {neq_zero_one : (not (EQ ZERO ONE))}
+      {phi_opp : forall a, eq (phi (OPP a)) (opp (phi a))}
+      {phi_add : forall a b, eq (phi (ADD a b)) (add (phi a) (phi b))}
+      {phi_sub : forall a b, eq (phi (SUB a b)) (sub (phi a) (phi b))}
+      {phi_mul : forall a b, eq (phi (MUL a b)) (mul (phi a) (phi b))}
+      {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
+      {phi_div : forall a b, eq (phi (DIV a b)) (div (phi a) (phi b))}
+      {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.
+
+Lemma equivalent_operations_field
+      {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
+      {EQ_equivalence : Equivalence EQ}
+      {zero one opp add sub mul inv div}
+      {fieldR:@field T EQ zero one opp add sub mul inv div}
+      {EQ_opp : forall a, EQ (OPP a) (opp a)}
+      {EQ_inv : forall a, EQ (INV a) (inv a)}
+      {EQ_add : forall a b, EQ (ADD a b) (add a b)}
+      {EQ_sub : forall a b, EQ (SUB a b) (sub a b)}
+      {EQ_mul : forall a b, EQ (MUL a b) (mul a b)}
+      {EQ_div : forall a b, EQ (DIV a b) (div a b)}
+      {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.
+
+Section Homomorphism.
+  Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}.
+  Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}.
+  Context {phi:F->K}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+  Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}.
+
+  Lemma homomorphism_multiplicative_inverse
+    : forall x, not (EQ x ZERO)
+                -> phi (INV x) = inv (phi x).
+  Proof.
+    intros.
+    eapply inv_unique.
+    rewrite <-Ring.homomorphism_mul.
+    rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
+  Qed.
+
+  Lemma homomorphism_multiplicative_inverse_complete
+        { EQ_dec : DecidableRel EQ }
+    : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x))
+                -> phi (INV x) = inv (phi x).
+  Proof.
+    intros x ?; destruct (dec (EQ x ZERO)); auto using homomorphism_multiplicative_inverse.
+  Qed.
+
+  Lemma homomorphism_div
+    : forall x y, not (EQ y ZERO)
+                  -> phi (DIV x y) = div (phi x) (phi y).
+  Proof.
+    intros. rewrite !field_div_definition.
+    rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse;
+      (eauto || reflexivity).
+  Qed.
+
+  Lemma homomorphism_div_complete
+        { EQ_dec : DecidableRel EQ }
+    : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y))
+                  -> phi (DIV x y) = div (phi x) (phi y).
+  Proof.
+    intros. rewrite !field_div_definition.
+    rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete;
+      (eauto || reflexivity).
+  Qed.
+End Homomorphism.
+
+Section Homomorphism_rev.
+  Context {F EQ ZERO ONE OPP ADD SUB MUL INV DIV} {fieldF:@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}.
+  Context {H} {eq : H -> H -> Prop} {zero one : H} {opp : H -> H} {add sub mul : H -> H -> H} {inv : H -> H} {div : H -> H -> H}.
+  Context {phi:F->H} {phi':H->F}.
+  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'_zero : phi' zero = ZERO}
+          {phi'_one : phi' one = ONE}
+          {phi'_opp : forall a, phi' (opp a) = OPP (phi' a)}
+          (phi'_add : forall a b, phi' (add a b) = ADD (phi' a) (phi' b))
+          (phi'_sub : forall a b, phi' (sub a b) = SUB (phi' a) (phi' b))
+          (phi'_mul : forall a b, phi' (mul a b) = MUL (phi' a) (phi' b))
+          {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
+          (phi'_div : forall a b, phi' (div a b) = DIV (phi' a) (phi' b)).
+
+  Lemma field_and_homomorphism_from_redundant_representation
+    : @field H eq zero one opp add sub mul inv div
+      /\ @Ring.is_homomorphism F EQ ONE ADD MUL H eq one add mul phi
+      /\ @Ring.is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'.
+  Proof.
+    repeat match goal with
+           | [ 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 : group |- _ ] => destruct H; try clear H
+           | [ H : monoid |- _ ] => destruct H; try clear H
+           | [ H : is_commutative |- _ ] => destruct H; try clear H
+           | [ H : is_left_multiplicative_inverse |- _ ] => destruct H; try clear H
+           | [ H : is_left_distributive |- _ ] => destruct H; try clear H
+           | [ H : is_right_distributive |- _ ] => destruct H; try clear H
+           | [ H : is_zero_neq_one |- _ ] => 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 _ _)%type |- _ ] => pose proof (fun pf => H (proj1 (@phi'_eq _ _) pf)); clear H
+           | [ H : EQ _ _ |- _ ] => rewrite H
+           | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id by reflexivity
+           | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id in H by reflexivity
+           | _ => solve [ eauto ]
+           end.
+  Qed.
+End Homomorphism_rev.
+
+Ltac guess_field :=
+  match goal with
+  | |- ?eq _ _ =>  constr:(_:Algebra.field (eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Algebra.field (eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Algebra.field (eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Algebra.field (eq:=eq))
+  end.
+
+Ltac goal_to_field_equality fld :=
+  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  match goal with
+  | [ |- eq _ _] => idtac
+  | [ |- not (eq ?x ?y) ] => apply not_exfalso; intro; goal_to_field_equality fld
+  | _ => exfalso;
+         match goal with
+         | H: not (eq _ _) |- _ => apply not_exfalso in H; apply H
+         | _ => apply (field_is_zero_neq_one(field:=fld))
+         end
+  end.
+
+Ltac _introduce_inverse fld d d_nz :=
+  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in
+  let one := match type of fld with Algebra.field(one:=?one) => one end in
+  let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in
+  match goal with [H: eq (mul d _) one |- _ ] => fail 1 | _ => idtac end;
+  let d_i := fresh "i" in
+  unique pose proof (right_multiplicative_inverse(H:=fld) _ d_nz);
+  set (inv d) as d_i in *;
+  clearbody d_i.
+
+Ltac inequalities_to_inverse_equations fld :=
+  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let div := match type of fld with Algebra.field(div:=?div) => div end in
+  let sub := match type of fld with Algebra.field(sub:=?sub) => sub end in
+  repeat match goal with
+         | [H: not (eq _ _) |- _ ] =>
+           lazymatch type of H with
+           | not (eq ?d zero) => _introduce_inverse fld d H
+           | not (eq zero ?d) => _introduce_inverse fld d (symmetry(R:=fun a b => not (eq a b)) H)
+           | not (eq ?x ?y) => _introduce_inverse fld (sub x y) (Ring.neq_sub_neq_zero _ _ H)
+           end
+         end.
+
+Ltac _nonzero_tac fld :=
+  solve [trivial | IntegralDomain.solve_constant_nonzero | goal_to_field_equality fld; nsatz; IntegralDomain.solve_constant_nonzero].
+
+Ltac _inverse_to_equation_by fld d tac :=
+  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let one := match type of fld with Algebra.field(one:=?one) => one end in
+  let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in
+  let div := match type of fld with Algebra.field(div:=?div) => div end in
+  let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in
+  let d_nz := fresh "nz" in
+  assert (not (eq d zero)) as d_nz by tac;
+  lazymatch goal with
+  | H: eq (mul ?di d) one |- _ => rewrite <-!(left_inv_unique(H:=fld) _ _ H) in *
+  | H: eq (mul d ?di) one |- _ => rewrite <-!(right_inv_unique(H:=fld) _ _ H) in *
+  | _ => _introduce_inverse constr:(fld) constr:(d) d_nz
+  end;
+  clear d_nz.
+
+Ltac inverses_to_equations_by fld tac :=
+  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in
+  repeat match goal with
+         | |- context[inv ?d] => _inverse_to_equation_by fld d tac
+         | H: context[inv ?d] |- _ => _inverse_to_equation_by fld d tac
+         end.
+
+Ltac divisions_to_inverses fld :=
+  rewrite ?(field_div_definition(field:=fld)) in *.
+
+Ltac fsatz :=
+  let fld := guess_field in
+  goal_to_field_equality fld;
+  inequalities_to_inverse_equations fld;
+  divisions_to_inverses fld;
+  inverses_to_equations_by fld ltac:(solve_debugfail ltac:(_nonzero_tac fld));
+  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.
+  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.
+  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.
+
+  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.
+  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
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
new file mode 100644
index 000000000..e4d38e243
--- /dev/null
+++ b/src/Algebra/Group.v
@@ -0,0 +1,247 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
+
+Section BasicProperties.
+  Context {T eq op id inv} `{@group T eq op id inv}.
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Infix "*" := op.
+  Local Infix "=" := eq : eq_scope.
+  Local Open Scope eq_scope.
+
+  Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
+  Proof. eauto using Monoid.cancel_left, left_inverse. Qed.
+  Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
+  Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
+  Lemma inv_inv x : inv(inv(x)) = x.
+  Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
+  Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
+  Proof. eauto using Monoid.inv_op, left_inverse. Qed.
+
+  Lemma inv_unique x ix : ix * x = id -> ix = inv x.
+  Proof.
+    intro Hix.
+    cut (ix*x*inv x = inv x).
+    - rewrite <-associative, right_inverse, right_identity; trivial.
+    - rewrite Hix, left_identity; reflexivity.
+  Qed.
+
+  Lemma move_leftL x y : inv y * x = id -> 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.
+  Qed.
+
+  Lemma inv_op x y : inv (x*y) = inv y*inv x.
+  Proof.
+    symmetry. etransitivity.
+    2:eapply inv_unique.
+    2:eapply inv_op_ext.
+    reflexivity.
+  Qed.
+
+  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.
+  Proof.
+    intros ? Hx Ho.
+    assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity).
+    rewrite Ho, right_identity in Hxo. intuition.
+  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 eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c.
+  Proof.
+    split; intro Hx; rewrite Hx || rewrite <-Hx;
+      rewrite <-!associative, ?left_inverse, ?right_inverse, right_identity;
+      reflexivity.
+  Qed.
+
+  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.
+    Lemma zero_neq_opp_one : id <> inv one.
+    Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
+  End ZeroNeqOne.
+End BasicProperties.
+
+Section Homomorphism.
+  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 {phi:G->H}`{homom:@Monoid.is_homomorphism G EQ OP H eq op phi}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+
+  Lemma homomorphism_id : phi ID = id.
+  Proof.
+    assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by
+        (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity).
+    rewrite cancel_left in Hii; exact Hii.
+  Qed.
+
+  Lemma homomorphism_inv x : phi (INV x) = inv (phi x).
+  Proof.
+    apply inv_unique.
+    rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity.
+  Qed.
+
+  Section ScalarMultHomomorphism.
+    Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }.
+    Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }.
+    Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P).
+    Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed.
+
+    Import ScalarMult.
+    Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P).
+    Proof.
+      induction n; intros.
+      { rewrite !scalarmult_0_l, inv_id; reflexivity. }
+      { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
+        rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. }
+    Qed.
+  End ScalarMultHomomorphism.
+End Homomorphism.
+
+Section Homomorphism_rev.
+  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
+  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}.
+
+  Local Instance group_from_redundant_representation
+    : @group H eq op id inv.
+  Proof.
+    repeat match goal with
+           | [ H : group |- _ ] => destruct H; try clear H
+           | [ H : monoid |- _ ] => 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 by reflexivity
+           | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity
+           | _ => solve [ eauto ]
+           end.
+  Qed.
+
+  Definition homomorphism_from_redundant_representation
+    : @Monoid.is_homomorphism G EQ OP H eq op phi.
+  Proof.
+    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 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.
+    split; repeat intro; rewrite <- !Hphi''.
+    { rewrite !Monoid.homomorphism; reflexivity. }
+    { apply Hphi', Hphi; assumption. }
+  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.
\ No newline at end of file
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
new file mode 100644
index 000000000..96a4cf06b
--- /dev/null
+++ b/src/Algebra/IntegralDomain.v
@@ -0,0 +1,155 @@
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Algebra Crypto.Algebra.Ring.
+
+Module IntegralDomain.
+  Section IntegralDomain.
+    Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}.
+
+    Lemma nonzero_product_iff_nonzero_factors :
+      forall x y : T, ~ eq (mul x y) zero <-> ~ eq x zero /\ ~ eq y zero.
+    Proof. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed.
+
+    Global Instance Integral_domain :
+      @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
+                                       Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
+    Proof. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
+  End IntegralDomain.
+
+  Module _LargeCharacteristicReflective.
+    Section ReflectiveNsatzSideConditionProver.
+      Import BinInt BinNat BinPos.
+      Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted.
+      Context {R eq zero one opp add sub mul}
+              {ring:@Algebra.ring R eq zero one opp add sub mul}
+              {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}.
+      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 Infix "+" := add.  Local Infix "-" := sub. Local Infix "*" := mul.
+      
+      Inductive coef :=
+      | Coef_one
+      | Coef_opp (_:coef)
+      | Coef_add (_ _:coef)
+      | Coef_mul (_ _:coef).
+      Fixpoint denote (c:coef) : R :=
+        match c with
+        | Coef_one => one
+        | Coef_opp c => opp (denote c)
+        | Coef_add c1 c2 => add (denote c1) (denote c2)
+        | Coef_mul c1 c2 => mul (denote c1) (denote c2)
+        end.
+      Fixpoint CtoZ (c:coef) : Z :=
+        match c with
+        | Coef_one => Z.one
+        | Coef_opp c => Z.opp (CtoZ c)
+        | Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2)
+        | Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2)
+        end.
+      Local Notation of_Z := (@Ring.of_Z R zero one opp add).
+
+      Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
+      Proof.
+        induction c; simpl CtoZ; simpl denote;
+          repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity.
+      Qed.
+
+      Section WithChar.
+        Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C).
+        Fixpoint is_nonzero (c:coef) : bool :=
+          match c with
+          | 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
+          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 *
+                   | _ => 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)
+                   | |- _ * _ <> 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)
+                   end.
+        Qed.
+      End WithChar.
+    End ReflectiveNsatzSideConditionProver.
+
+    Ltac reify one opp add mul x :=
+      match x with
+      | one => constr:(Coef_one)
+      | opp ?a =>
+        let a := reify one opp add mul a in
+        constr:(Coef_opp a)
+      | add ?a ?b =>
+        let a := reify one opp add mul a in
+        let b := reify one opp add mul b in
+        constr:(Coef_add a b)
+      | mul ?a ?b =>
+        let a := reify one opp add mul a in
+        let b := reify one opp add mul b in
+        constr:(Coef_mul a b)
+      end.
+  End _LargeCharacteristicReflective.
+
+  Ltac solve_constant_nonzero :=
+    match goal with (* TODO: change this match to a typeclass resolution *)
+    | |- not (?eq ?x _) =>
+      let cg := constr:(_:Ring.char_gt (eq:=eq) _) in
+      match type of cg with
+        @Ring.char_gt ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C =>
+        let x' := _LargeCharacteristicReflective.reify one opp add mul x in
+        let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in
+        change (not (eq x' zero));
+        apply (_LargeCharacteristicReflective.is_nonzero_correct(eq:=eq)(zero:=zero) C cg);
+        abstract (vm_cast_no_check (eq_refl true))
+      end
+    end.
+End IntegralDomain.
+
+(** Tactics for polynomial equations over integral domains *)
+
+Require Coq.nsatz.Nsatz.
+
+Ltac dropAlgebraSyntax :=
+  cbv beta delta [
+      Algebra_syntax.zero
+        Algebra_syntax.one
+        Algebra_syntax.addition
+        Algebra_syntax.multiplication
+        Algebra_syntax.subtraction
+        Algebra_syntax.opposite
+        Algebra_syntax.equality
+        Algebra_syntax.bracket
+        Algebra_syntax.power
+        ] in *.
+
+Ltac dropRingSyntax :=
+  dropAlgebraSyntax;
+  cbv beta delta [
+      Ncring.zero_notation
+        Ncring.one_notation
+        Ncring.add_notation
+        Ncring.mul_notation
+        Ncring.sub_notation
+        Ncring.opp_notation
+        Ncring.eq_notation
+    ] in *.
+Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
new file mode 100644
index 000000000..f71efff3e
--- /dev/null
+++ b/src/Algebra/Monoid.v
@@ -0,0 +1,60 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Algebra.
+
+Section Monoid.
+  Context {T eq op id} {monoid:@monoid T eq op id}.
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Infix "*" := op.
+  Local Infix "=" := eq : eq_scope.
+  Local Open Scope eq_scope.
+
+  Lemma cancel_right z iz (Hinv:op z iz = id) :
+    forall x y, x * z = y * z <-> x = y.
+  Proof.
+    split; intros.
+    { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity).
+      rewrite <-associative in Hcut.
+      rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
+    { rewrite_hyp ->!*. reflexivity. }
+  Qed.
+
+  Lemma cancel_left z iz (Hinv:op iz z = id) :
+    forall x y, z * x = z * y <-> x = y.
+  Proof.
+    split; intros.
+    { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity).
+      rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
+    { rewrite_hyp ->!*; reflexivity. }
+  Qed.
+
+  Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x.
+  Proof.
+    intros Hi Hii.
+    assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity).
+    rewrite associative, Hii, left_identity, right_identity in H; exact H.
+  Qed.
+
+  Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id.
+  Proof.
+    intros Hx Hy.
+    cut (iy * (ix*x) * y = id); try intro H.
+    { rewrite <-!associative; rewrite <-!associative in H; exact H. }
+    rewrite Hx, right_identity, Hy. reflexivity.
+  Qed.
+
+End Monoid.
+
+Section Homomorphism.
+  Context {T  EQ OP ID} {monoidT:  @monoid T  EQ OP ID }.
+  Context {T' eq op id} {monoidT': @monoid T' eq op id }.
+  Context {phi:T->T'}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+  Class is_homomorphism :=
+    {
+      homomorphism : forall a b,  phi (OP a b) = op (phi a) (phi b);
+
+      is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
+    }.
+  Global Existing Instance is_homomorphism_phi_proper.
+End Homomorphism.
\ No newline at end of file
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
new file mode 100644
index 000000000..2d8061ddc
--- /dev/null
+++ b/src/Algebra/Ring.v
@@ -0,0 +1,369 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid.
+Require Coq.ZArith.ZArith Coq.PArith.PArith.
+
+Section Ring.
+  Context {T eq zero one opp add sub mul} `{@ring T eq zero one opp add sub mul}.
+  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 "-" := sub. Local Infix "*" := mul.
+
+  Lemma mul_0_l : forall x, 0 * x = 0.
+  Proof.
+    intros.
+    assert (0*x = 0*x) as Hx by reflexivity.
+    rewrite <-(right_identity 0), right_distributive in Hx at 1.
+    assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (rewrite Hx; reflexivity).
+    rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx.
+  Qed.
+
+  Lemma mul_0_r : forall x, x * 0 = 0.
+  Proof.
+    intros.
+    assert (x*0 = x*0) as Hx by reflexivity.
+    rewrite <-(left_identity 0), left_distributive in Hx at 1.
+    assert (opp (x*0) + (x*0 + x*0)  = opp (x*0) + x*0) as Hxx by (rewrite Hx; reflexivity).
+    rewrite associative, left_inverse, left_identity in Hxx; exact Hxx.
+  Qed.
+
+  Lemma sub_0_l x : 0 - x = opp x.
+  Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed.
+
+  Lemma mul_opp_r x y : x * opp y = opp (x * y).
+  Proof.
+    assert (Ho:x*(opp y) + x*y = 0)
+      by (rewrite <-left_distributive, left_inverse, mul_0_r; reflexivity).
+    rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
+    rewrite <-!associative, right_inverse, right_identity; reflexivity.
+  Qed.
+
+  Lemma mul_opp_l x y : opp x * y = opp (x * y).
+  Proof.
+    assert (Ho:opp x*y + x*y = 0)
+      by (rewrite <-right_distributive, left_inverse, mul_0_l; reflexivity).
+    rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
+    rewrite <-!associative, right_inverse, right_identity; reflexivity.
+  Qed.
+
+  Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero.
+
+  Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul).
+  Proof.
+    split; intros. rewrite !ring_sub_definition, left_distributive.
+    eapply Group.cancel_left, mul_opp_r.
+  Qed.
+
+  Global Instance is_right_distributive_sub : is_right_distributive (eq:=eq)(add:=sub)(mul:=mul).
+  Proof.
+    split; intros. rewrite !ring_sub_definition, right_distributive.
+    eapply Group.cancel_left, mul_opp_l.
+  Qed.
+
+  Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0.
+  Proof.
+    intro Hsub. apply Hxy. rewrite <-(left_identity y), <-Hsub, ring_sub_definition.
+    rewrite <-associative, left_inverse, right_identity. reflexivity.
+  Qed.
+
+  Lemma zero_product_iff_zero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
+    forall x y : T, eq (mul x y) zero <-> eq x zero \/ eq y zero.
+  Proof.
+    split; eauto using zero_product_zero_factor; [].
+    intros [Hz|Hz]; rewrite Hz; eauto using mul_0_l, mul_0_r.
+  Qed.
+
+  Lemma nonzero_product_iff_nonzero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
+    forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)).
+  Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
+
+  Lemma nonzero_hypothesis_to_goal {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
+    forall x y : T, (not (eq x zero) -> eq y zero) <-> (eq (mul x y) zero).
+  Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
+
+  Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq.
+  Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
+  Proof.
+    split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances.
+    - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *)
+      eapply @left_identity; eauto with typeclass_instances.
+    - eapply @right_identity; eauto with typeclass_instances.
+    - eapply associative.
+    - intros; eapply right_distributive.
+    - intros; eapply left_distributive.
+  Qed.
+End Ring.
+
+Section Homomorphism.
+  Context {R EQ ZERO ONE OPP ADD SUB MUL} `{@ring R EQ ZERO ONE OPP ADD SUB MUL}.
+  Context {S eq zero one opp add sub mul} `{@ring S eq zero one opp add sub mul}.
+  Context {phi:R->S}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+
+  Class is_homomorphism :=
+    {
+      homomorphism_is_homomorphism : Monoid.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq);
+      homomorphism_mul : forall x y, phi (MUL x y) = mul (phi x) (phi y);
+      homomorphism_one : phi ONE = one
+    }.
+  Global Existing Instance homomorphism_is_homomorphism.
+
+  Context `{phi_homom:is_homomorphism}.
+
+  Lemma homomorphism_zero : phi ZERO = zero.
+  Proof. apply Group.homomorphism_id. Qed.
+
+  Lemma homomorphism_add : forall x y,  phi (ADD x y) = add (phi x) (phi y).
+  Proof. apply Monoid.homomorphism. Qed.
+
+  Definition homomorphism_opp : forall x,  phi (OPP x) = opp (phi x) :=
+    (Group.homomorphism_inv (INV:=OPP) (inv:=opp)).
+
+  Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y).
+  Proof.
+    intros.
+    rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity.
+  Qed.
+End Homomorphism.
+
+Ltac push_homomorphism phi :=
+  let H := constr:(_:is_homomorphism(phi:=phi)) in
+  repeat rewrite
+         ?(homomorphism_zero(     phi_homom:=H)),
+         ?(homomorphism_one(is_homomorphism:=H)),
+         ?(homomorphism_add(      phi_homom:=H)),
+         ?(homomorphism_opp(      phi_homom:=H)),
+         ?(homomorphism_sub(      phi_homom:=H)),
+         ?(homomorphism_mul(is_homomorphism:=H)).
+
+Lemma isomorphism_to_subring_ring
+      {T EQ ZERO ONE OPP ADD SUB MUL}
+      {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
+      {Proper_OPP:Proper(EQ==>EQ)OPP}
+      {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
+      {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
+      {Proper_MUL:Proper(EQ==>EQ==>EQ)MUL}
+      {R eq zero one opp add sub mul} {ringR:@ring R eq zero one opp add sub mul}
+      {phi}
+      {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
+      {phi_opp : forall a, eq (phi (OPP a)) (opp (phi a))}
+      {phi_add : forall a b, eq (phi (ADD a b)) (add (phi a) (phi b))}
+      {phi_sub : forall a b, eq (phi (SUB a b)) (sub (phi a) (phi b))}
+      {phi_mul : forall a b, eq (phi (MUL a b)) (mul (phi a) (phi b))}
+      {phi_zero : eq (phi ZERO) zero}
+      {phi_one : eq (phi ONE) one}
+  : @ring T EQ ZERO ONE OPP ADD SUB MUL.
+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;
+    auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)),
+    (associative (op := mul)), (commutative (op := add)), (left_identity (op := mul)), (right_identity (op := mul)),
+    left_inverse, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)), ring_sub_definition.
+Qed.
+
+Section TacticSupportCommutative.
+  Context {T eq zero one opp add sub mul} `{@commutative_ring T eq zero one opp add sub mul}.
+
+  Global Instance Cring_Cring_commutative_ring :
+    @Cring.Cring T zero one add mul sub opp eq Ncring_Ring_ops Ncring_Ring.
+  Proof. unfold Cring.Cring; intros; cbv. eapply commutative. Qed.
+
+  Lemma ring_theory_for_stdlib_tactic : Ring_theory.ring_theory zero one add mul sub opp eq.
+  Proof.
+    constructor; intros. (* TODO(automation): make [auto] do this? *)
+    - apply left_identity.
+    - apply commutative.
+    - apply associative.
+    - apply left_identity.
+    - apply commutative.
+    - apply associative.
+    - apply right_distributive.
+    - apply ring_sub_definition.
+    - apply right_inverse.
+  Qed.
+End TacticSupportCommutative.
+
+Section Z.
+  Import ZArith.
+  Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed.
+
+  Global Instance commutative_ring_Z : @commutative_ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. eauto using @commutative_ring, @is_commutative, ring_Z with zarith. Qed.
+
+  Global Instance integral_domain_Z : @integral_domain Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof.
+    split.
+    { apply commutative_ring_Z. }
+    { split. intros. eapply Z.eq_mul_0; assumption. }
+    { split. discriminate. }
+  Qed.
+End Z.
+
+Section of_Z.
+  Import ZArith PArith. Local Open Scope Z_scope.
+  Context {R Req Rzero Rone Ropp Radd Rsub Rmul}
+          {Rring : @ring R Req Rzero Rone Ropp Radd Rsub Rmul}.
+  Local Infix "=" := Req. Local Infix "=" := Req : type_scope.
+
+  Fixpoint of_nat (n:nat) : R :=
+    match n with
+    | O => Rzero
+    | S n' => Radd (of_nat n') Rone
+    end.
+  Definition of_Z (x:Z) : R :=
+    match x with
+    | Z0 => Rzero
+    | Zpos p => of_nat (Pos.to_nat p)
+    | Zneg p => Ropp (of_nat (Pos.to_nat p))
+    end.
+
+  Lemma of_Z_0 : of_Z 0 = Rzero.
+  Proof. reflexivity. Qed.
+
+  Lemma of_nat_add x :
+    of_nat (Nat.add x 1) = Radd (of_nat x) Rone.
+  Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed.
+
+  Lemma of_nat_sub x (H: (0 < x)%nat):
+    of_nat (Nat.sub x 1) = Rsub (of_nat x) Rone.
+  Proof.
+    induction x; [omega|simpl].
+    rewrite <-of_nat_add.
+    rewrite Nat.sub_0_r, Nat.add_1_r.
+    simpl of_nat.
+    rewrite ring_sub_definition, <-associative.
+    rewrite right_inverse, right_identity.
+    reflexivity.
+  Qed.
+
+  Lemma of_Z_add_1_r :
+    forall x, of_Z (Z.add x 1) = Radd (of_Z x) Rone.
+  Proof.
+    destruct x; [reflexivity| | ]; simpl of_Z.
+    { rewrite Pos2Nat.inj_add, of_nat_add.
+      reflexivity. }
+    { rewrite Z.pos_sub_spec; break_match;
+        match goal with
+        | H : _ |- _ => rewrite Pos.compare_eq_iff in H
+        | H : _ |- _ => rewrite Pos.compare_lt_iff in H
+        | H : _ |- _ => rewrite Pos.compare_gt_iff in H;
+                          apply Pos.nlt_1_r in H; tauto
+        end;
+        subst; simpl of_Z; simpl of_nat.
+      { rewrite left_identity, left_inverse; reflexivity. }
+      { rewrite Pos2Nat.inj_sub by assumption.
+        rewrite of_nat_sub by apply Pos2Nat.is_pos.
+        rewrite ring_sub_definition, Group.inv_op, Group.inv_inv.
+        rewrite commutative; reflexivity. } }
+  Qed.
+
+  Lemma of_Z_sub_1_r :
+    forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone.
+  Proof.
+    induction x.
+    { simpl; rewrite ring_sub_definition, !left_identity;
+        reflexivity. }
+    { case_eq (1 ?= p)%positive; intros;
+        match goal with
+        | H : _ |- _ => rewrite Pos.compare_eq_iff in H
+        | H : _ |- _ => rewrite Pos.compare_lt_iff in H
+        | H : _ |- _ => rewrite Pos.compare_gt_iff in H;
+                          apply Pos.nlt_1_r in H; tauto
+        end.
+      { subst. simpl; rewrite ring_sub_definition, !left_identity,
+                      right_inverse; reflexivity. }
+      { rewrite <-Pos2Z.inj_sub by assumption; simpl of_Z.
+        rewrite Pos2Nat.inj_sub by assumption.
+        rewrite of_nat_sub by apply Pos2Nat.is_pos.
+        reflexivity. } }
+    { simpl. rewrite Pos2Nat.inj_add, of_nat_add.
+      rewrite ring_sub_definition, Group.inv_op, commutative.
+      reflexivity. }
+  Qed.
+
+  Lemma of_Z_opp : forall a,
+      of_Z (Z.opp a) = Ropp (of_Z a).
+  Proof.
+    destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv;
+      reflexivity.
+  Qed.
+
+  Lemma of_Z_add : forall a b,
+      of_Z (Z.add a b) = Radd (of_Z a) (of_Z b).
+  Proof.
+    intros.
+    let x := match goal with |- ?x => x end in
+    let f := match (eval pattern b in x) with ?f _ => f end in
+    apply (Z.peano_ind f); intros.
+    { rewrite !right_identity. reflexivity. }
+    { replace (a + Z.succ x) with ((a + x) + 1) by ring.
+      replace (Z.succ x) with (x+1) by ring.
+      rewrite !of_Z_add_1_r, H.
+      rewrite associative; reflexivity. }
+    { replace (a + Z.pred x) with ((a+x)-1)
+        by (rewrite <-Z.sub_1_r; ring).
+      replace (Z.pred x) with (x-1) by apply Z.sub_1_r.
+      rewrite !of_Z_sub_1_r, H.
+      rewrite !ring_sub_definition.
+      rewrite associative; reflexivity. }
+  Qed.
+
+  Lemma of_Z_mul : forall a b,
+      of_Z (Z.mul a b) = Rmul (of_Z a) (of_Z b).
+  Proof.
+    intros.
+    let x := match goal with |- ?x => x end in
+    let f := match (eval pattern b in x) with ?f _ => f end in
+    apply (Z.peano_ind f); intros until 0; try intro IHb.
+    { rewrite !mul_0_r; reflexivity. }
+    { rewrite Z.mul_succ_r, <-Z.add_1_r.
+      rewrite of_Z_add, of_Z_add_1_r.
+      rewrite IHb.
+      rewrite left_distributive, right_identity.
+      reflexivity. }
+    { rewrite Z.mul_pred_r, <-Z.sub_1_r.
+      rewrite of_Z_sub_1_r.
+      rewrite <-Z.add_opp_r.
+      rewrite of_Z_add, of_Z_opp.
+      rewrite IHb.
+      rewrite ring_sub_definition, left_distributive.
+      rewrite mul_opp_r,right_identity.
+      reflexivity. }
+  Qed.
+
+
+  Global Instance homomorphism_of_Z :
+    @is_homomorphism
+      Z Logic.eq Z.one Z.add Z.mul
+      R Req  Rone  Radd  Rmul
+      of_Z.
+  Proof.
+    repeat constructor; intros.
+    { apply of_Z_add. }
+    { repeat intro; subst; reflexivity. }
+    { apply of_Z_mul. }
+    { simpl. rewrite left_identity; reflexivity. }
+  Qed.
+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.
+Existing Class char_gt.
+
+(*** Tactics for ring equations *)
+Require Export Coq.setoid_ring.Ring_tac.
+Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
+
+Ltac ring_simplify_subterms_in_all :=
+  reverse_nondep; ring_simplify_subterms; intros.
+
+Create HintDb ring_simplify discriminated.
+Create HintDb ring_simplify_subterms discriminated.
+Create HintDb ring_simplify_subterms_in_all discriminated.
+Hint Extern 1 => progress ring_simplify : ring_simplify.
+Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms.
+Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all.
\ No newline at end of file
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
new file mode 100644
index 000000000..33c236775
--- /dev/null
+++ b/src/Algebra/ScalarMult.v
@@ -0,0 +1,90 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Algebra Crypto.Algebra.Monoid.
+
+Module Import ModuloCoq8485.
+  Import NPeano Nat.
+  Infix "mod" := modulo.
+End ModuloCoq8485.
+
+Section ScalarMultProperties.
+  Context {G eq add zero} `{monoidG:@monoid G eq add zero}.
+  Context {mul:nat->G->G}.
+  Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
+  Local Infix "+" := add. Local Infix "*" := mul.
+  Class is_scalarmult :=
+    {
+      scalarmult_0_l : forall P, 0 * P = zero;
+      scalarmult_S_l : forall n P, S n * P = P + n * P;
+
+      scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul
+    }.
+  Global Existing Instance scalarmult_Proper.
+  Context `{mul_is_scalarmult:is_scalarmult}.
+
+  Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} :=
+    match n with
+    | O => zero
+    | S n' => add P (scalarmult_ref n' P)
+    end.
+
+  Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
+  Proof.
+    repeat intro; subst.
+    match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
+    repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
+  Qed.
+
+  Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
+    induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
+  Qed.
+
+  Lemma scalarmult_1_l : forall P, 1*P = P.
+  Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
+
+  Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
+  Proof.
+    induction n; intros;
+      rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+  Qed.
+
+  Lemma scalarmult_zero_r : forall m, m * zero = zero.
+  Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+
+  Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
+  Proof.
+    induction n; intros.
+    { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
+    { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l.
+      rewrite IHn. reflexivity. }
+  Qed.
+
+  Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
+  Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
+
+  Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
+  Proof.
+    intros ? ? Hnz Hmod ?.
+    rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
+    rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
+  Qed.
+End ScalarMultProperties.
+
+Section ScalarMultHomomorphism.
+  Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}.
+  Context {H eq add zero} {monoidH:@monoid H eq add zero}.
+  Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope.
+  Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }.
+  Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }.
+  Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}.
+  Context (phi_ZERO:phi ZERO = zero).
+
+  Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P).
+  Proof.
+    setoid_rewrite scalarmult_ext.
+    induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy.
+  Qed.
+End ScalarMultHomomorphism.
+
+Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
+  : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
+Proof. split; try exact _; intros; reflexivity. Qed.
\ No newline at end of file
diff --git a/src/Algebra/ZToRing.v b/src/Algebra/ZToRing.v
deleted file mode 100644
index 0c423222e..000000000
--- a/src/Algebra/ZToRing.v
+++ /dev/null
@@ -1,150 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.PArith.PArith.
-Require Import Crypto.Algebra.
-Require Import Crypto.Util.Tactics.
-Local Open Scope Z_scope.
-
-Section ZToRing.
-  Context {R Req Rzero Rone Ropp Radd Rsub Rmul}
-          {Rring : @ring R Req Rzero Rone Ropp Radd Rsub Rmul}.
-  Local Infix "=" := Req. Local Infix "=" := Req : type_scope.
-
-  Fixpoint natToRing (n:nat) : R :=
-    match n with
-    | O => Rzero
-    | S n' => Radd (natToRing n') Rone
-    end.
-  Definition ZToRing (x:Z) : R :=
-    match x with
-    | Z0 => Rzero
-    | Zpos p => natToRing (Pos.to_nat p)
-    | Zneg p => Ropp (natToRing (Pos.to_nat p))
-    end.
-
-  Lemma ZToRing_zero_correct : ZToRing 0 = Rzero.
-  Proof. reflexivity. Qed.
-
-  Lemma natToRing_plus_correct x :
-    natToRing (Nat.add x 1) = Radd (natToRing x) Rone.
-  Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed.
-
-  Lemma natToRing_minus_correct x (H: (0 < x)%nat):
-    natToRing (Nat.sub x 1) = Rsub (natToRing x) Rone.
-  Proof.
-    induction x; [omega|simpl].
-    rewrite <-natToRing_plus_correct.
-    rewrite Nat.sub_0_r, Nat.add_1_r.
-    simpl natToRing.
-    rewrite ring_sub_definition, <-associative.
-    rewrite right_inverse, right_identity.
-    reflexivity.
-  Qed.
-
-  Lemma ZToRing_plus_correct :
-    forall x, ZToRing (Z.add x 1) = Radd (ZToRing x) Rone.
-  Proof.
-    destruct x; [reflexivity| | ]; simpl ZToRing.
-    { rewrite Pos2Nat.inj_add, natToRing_plus_correct.
-      reflexivity. }
-    { rewrite Z.pos_sub_spec; break_match;
-        match goal with
-        | H : _ |- _ => rewrite Pos.compare_eq_iff in H
-        | H : _ |- _ => rewrite Pos.compare_lt_iff in H
-        | H : _ |- _ => rewrite Pos.compare_gt_iff in H;
-                          apply Pos.nlt_1_r in H; tauto
-        end;
-        subst; simpl ZToRing; simpl natToRing.
-      { rewrite left_identity, left_inverse; reflexivity. }
-      { rewrite Pos2Nat.inj_sub by assumption.
-        rewrite natToRing_minus_correct by apply Pos2Nat.is_pos.
-        rewrite ring_sub_definition, Group.inv_op, Group.inv_inv.
-        rewrite commutative; reflexivity. } }
-  Qed.
-
-  Lemma ZToRing_minus_correct :
-    forall x, ZToRing (Z.sub x 1) = Rsub (ZToRing x) Rone.
-  Proof.
-    induction x.
-    { simpl; rewrite ring_sub_definition, !left_identity;
-        reflexivity. }
-    { case_eq (1 ?= p)%positive; intros;
-        match goal with
-        | H : _ |- _ => rewrite Pos.compare_eq_iff in H
-        | H : _ |- _ => rewrite Pos.compare_lt_iff in H
-        | H : _ |- _ => rewrite Pos.compare_gt_iff in H;
-                          apply Pos.nlt_1_r in H; tauto
-        end.
-      { subst. simpl; rewrite ring_sub_definition, !left_identity,
-                      right_inverse; reflexivity. }
-      { rewrite <-Pos2Z.inj_sub by assumption; simpl ZToRing.
-        rewrite Pos2Nat.inj_sub by assumption.
-        rewrite natToRing_minus_correct by apply Pos2Nat.is_pos.
-        reflexivity. } }
-    { simpl. rewrite Pos2Nat.inj_add, natToRing_plus_correct.
-      rewrite ring_sub_definition, Group.inv_op, commutative.
-      reflexivity. }
-  Qed.
-
-  Lemma ZToRing_inj_opp : forall a,
-      ZToRing (Z.opp a) = Ropp (ZToRing a).
-  Proof.
-    destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv;
-      reflexivity.
-  Qed.
-
-  Lemma ZToRing_inj_add : forall a b,
-      ZToRing (Z.add a b) = Radd (ZToRing a) (ZToRing b).
-  Proof.
-    intros.
-    let x := match goal with |- ?x => x end in
-    let f := match (eval pattern b in x) with ?f _ => f end in
-    apply (Z.peano_ind f); intros.
-    { rewrite !right_identity; reflexivity. }
-    { replace (a + Z.succ x) with ((a + x) + 1) by ring.
-      replace (Z.succ x) with (x+1) by ring.
-      rewrite !ZToRing_plus_correct, H.
-      rewrite associative; reflexivity. }
-    { replace (a + Z.pred x) with ((a+x)-1)
-        by (rewrite <-Z.sub_1_r; ring).
-      replace (Z.pred x) with (x-1) by apply Z.sub_1_r.
-      rewrite !ZToRing_minus_correct, H.
-      rewrite !ring_sub_definition.
-      rewrite associative; reflexivity. }
-  Qed.
-
-  Lemma ZToRing_inj_mul : forall a b,
-      ZToRing (Z.mul a b) = Rmul (ZToRing a) (ZToRing b).
-  Proof.
-    intros.
-    let x := match goal with |- ?x => x end in
-    let f := match (eval pattern b in x) with ?f _ => f end in
-    apply (Z.peano_ind f); intros until 0; try intro IHb.
-    { rewrite !Ring.mul_0_r; reflexivity. }
-    { rewrite Z.mul_succ_r, <-Z.add_1_r.
-      rewrite ZToRing_inj_add, ZToRing_plus_correct.
-      rewrite IHb.
-      rewrite left_distributive, right_identity.
-      reflexivity. }
-    { rewrite Z.mul_pred_r, <-Z.sub_1_r.
-      rewrite ZToRing_minus_correct.
-      rewrite <-Z.add_opp_r.
-      rewrite ZToRing_inj_add, ZToRing_inj_opp.
-      rewrite IHb.
-      rewrite ring_sub_definition, left_distributive.
-      rewrite Ring.mul_opp_r,right_identity.
-      reflexivity. }
-  Qed.
-
-
-  Lemma ZToRingHomom : @Ring.is_homomorphism
-                         Z Z.eq Z.one Z.add Z.mul
-                         R Req  Rone  Radd  Rmul
-                         ZToRing.
-  Proof.
-    repeat constructor; intros.
-    { apply ZToRing_inj_add. }
-    { repeat intro. cbv [Z.eq] in *. subst. reflexivity. }
-    { apply ZToRing_inj_mul. }
-    { simpl. rewrite left_identity; reflexivity. }
-  Qed.
-End ZToRing.