Refactor ModularArithmetic into Zmod, expand Decidable

ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.

Backwards-incompatible changes:

F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1

8 files changed, 534 insertions, 1321 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index be9307b50..e36d15c8b 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -2,54 +2,20 @@ Require Import Coq.omega.Omega.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.Pre.
 
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
-Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
-Require Export Crypto.Util.IterAssocOp.
+Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac.
 
+Require Import Crypto.Algebra Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 
-Section ModularArithmeticPreliminaries.
-  Context {m:Z}.
-  Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
-
-  Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
-  Proof.
-    destruct x, y; intuition; simpl in *; try congruence.
-    subst_max.
-    f_equal.
-    eapply UIP_dec, Z.eq_dec.
-  Qed.
-
-  Lemma F_pow_spec : forall (a:F m),
-      pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
-  Proof.
-    intros a.
-    pose (@pow_with_spec m) as H.
-    change (@pow m) with (proj1_sig H).
-    destruct H; eauto.
-  Qed.
-End ModularArithmeticPreliminaries.
-
 (* Fails iff the input term does some arithmetic with mod'd values. *)
 Ltac notFancy E :=
-match E with
-| - (_ mod _) => idtac
-| context[_ mod _] => fail 1
-| _ => idtac
-end.
-
-Lemma Zplus_neg : forall n m, n + -m = n - m.
-Proof.
-  auto.
-Qed.
-
-Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n.
-Proof.
-  intros; rewrite H; trivial.
-Qed.
+  match E with
+  | - (_ mod _) => idtac
+  | context[_ mod _] => fail 1
+  | _ => idtac
+  end.
 
 (* Remove redundant [mod] operations from the conclusion. *)
 Ltac demod :=
@@ -68,680 +34,325 @@ Ltac demod :=
            notFancy y; rewrite (Zmult_mod_idemp_r y)
          | [ |- context[(?x mod _) mod _] ] =>
            notFancy x; rewrite (Zmod_mod x)
-         | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in *
          end.
 
-(* Remove exists under equals: we do this a lot *)
-Ltac eq_remove_proofs := lazymatch goal with
-| [ |- @eq (F _) ?a ?b ] =>
-    assert (Q := F_eq a b);
-    simpl in *; apply Q; clear Q
-end.
-
-(** TODO FIXME(from jgross): This tactic is way too powerful for
-    arcane reasons.  It should not be using so many databases with
-    [intuition]. *)
-Ltac Fdefn :=
+Ltac unwrap_F :=
   intros;
   repeat match goal with [ x : F _ |- _ ] => destruct x end;
-  try eq_remove_proofs;
-  demod;
-  rewrite ?Z.mul_1_l;
-  intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ].
-
-Local Open Scope F_scope.
-
-Section FEquality.
-  Context {m:Z}.
-
-  (** Equality **)
-  Definition F_eqb (x y : F m) : bool :=  Z.eqb x y.
-
-  Lemma F_eqb_eq x y : F_eqb x y = true -> x = y.
-  Proof.
-    unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial.
-  Qed.
-
-  Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true.
-  Proof.
-    intros; subst; apply Z.eqb_refl.
-  Qed.
-
-  Lemma F_eqb_refl : forall x, F_eqb x x = true.
-  Proof.
-    intros; apply F_eqb_complete; trivial.
-  Qed.
-
-  Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y.
-  Proof.
-    intuition; subst y.
-    pose proof (F_eqb_refl x).
-    congruence.
-  Qed.
-
-  Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false.
-  Proof.
-    intros.
-    case_eq (F_eqb x y); intros; trivial.
-    pose proof (F_eqb_eq x y); intuition.
-  Qed.
-
-  Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}.
-  Proof.
-    intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq.
-  Qed.
-
-  Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b).
-  Proof.
-    intros; intuition; break_if.
-    - rewrite F_eqb_complete; trivial.
-    - rewrite F_eqb_neq_complete; trivial.
-  Defined.
-End FEquality.
-
-Section FandZ.
-  Context {m:Z}.
-
-  Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m).
-  Proof.
-    intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith.
-  Qed.
-
-  Require Crypto.Algebra.
-  Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.
-  Proof.
-    repeat split; Fdefn; try apply F_eq_dec.
-    { rewrite Z.add_0_r. auto. }
-    { rewrite Z.mul_1_r. auto. }
-  Qed.
-
-  Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
-    Fdefn.
-  Qed.
-
-  Lemma ZToField_0 : @ZToField m 0 = 0.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma mod_FieldToZ : forall x,  (@FieldToZ m x) mod m = FieldToZ x.
-  Proof.
-    Fdefn.
-  Qed.
-
-  (** ZToField distributes over operations **)
-  Lemma ZToField_add : forall (x y : Z),
-      @ZToField m (x + y) = ZToField x + ZToField y.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma FieldToZ_add : forall x y : F m,
-      FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma FieldToZ_mul : forall x y : F m,
-      FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma FieldToZ_pow_Zpow_mod : forall (x : F m) n,
-    (FieldToZ x ^ Z.of_N n mod m = FieldToZ (x ^ n)%F)%Z.
-  Proof.
-    intros.
-    induction n using N.peano_ind;
-      destruct (F_pow_spec x) as [pow_0 pow_succ] . {
-      rewrite pow_0.
-      rewrite Z.pow_0_r; auto.
-    } {
-      rewrite N2Z.inj_succ.
-      rewrite Z.pow_succ_r by apply N2Z.is_nonneg.
-      rewrite <- N.add_1_l.
-      rewrite pow_succ.
-      rewrite <- Zmult_mod_idemp_r.
-      rewrite IHn.
-      apply FieldToZ_mul.
-    }
-  Qed.
-
-  Lemma FieldToZ_pow_efficient : forall (x : F m) n, FieldToZ (x^n) = powmod m (FieldToZ x) n.
-  Proof.
-    intros.
-    rewrite powmod_Zpow_mod.
-    rewrite <-FieldToZ_pow_Zpow_mod.
-    reflexivity.
-  Qed.
-
-  Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n.
-  Proof.
-    induction n using N.peano_ind;
-      destruct (F_pow_spec x) as [pow_0 pow_succ];
-      rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ;
-      simpl; congruence.
-  Qed.
-
-  Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->
-                                     b mod m =  (- a)  mod m.
-  Proof.
-    rewrite <-Z.sub_0_l; intros.
-    replace (0-a)%Z with (b-(a + b))%Z by omega.
-    rewrite Zminus_mod.
-    rewrite <- H.
-    rewrite Zmod_0_l.
-    replace (b mod m - 0)%Z with (b mod m) by omega.
-    rewrite Zmod_mod.
-    reflexivity.
-  Qed.
-
-  Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m.
-  Proof.
-    intros.
-    pose proof (FieldToZ_add x (opp x)) as H.
-    rewrite F_opp_spec, FieldToZ_ZToField in H.
-    auto using mod_plus_zero_subproof.
-  Qed.
-
-  Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m.
-  Proof.
-    intros.
-    pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial.
-  Qed.
-
-  Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.
-  Proof.
-    intros.
-    replace (x + (m - y))%Z with (m+(x-y))%Z by omega.
-    rewrite Zplus_mod.
-    rewrite Z_mod_same_full; simpl Z.add.
-    rewrite Zmod_mod.
-    reflexivity.
-  Qed.
-
-  (* Compatibility between inject and subtraction *)
-  Lemma ZToField_sub : forall (x y : Z),
-      @ZToField m (x - y) = ZToField x - ZToField y.
-  Proof.
-    Fdefn.
-  Qed.
-
-  (* Compatibility between inject and multiplication *)
-  Lemma ZToField_mul : forall (x y : Z),
-      @ZToField m (x * y) = ZToField x * ZToField y.
-  Proof.
-    Fdefn.
-  Qed.
-
-  (* Compatibility between inject and GFtoZ *)
-  Lemma ZToField_idempotent : forall (x : F m), ZToField x = x.
-  Proof.
-    Fdefn.
-  Qed.
-  Definition ZToField_FieldToZ := ZToField_idempotent. (* alias *)
-
-  (* Compatibility between inject and mod *)
-  Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m).
-  Proof.
-    Fdefn.
-  Qed.
-
-  (* Compatibility between inject and pow *)
-  Lemma ZToField_pow : forall x n,
-    @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m).
-  Proof.
-    intros.
-    induction n using N.peano_ind;
-      destruct (F_pow_spec (@ZToField m x)) as [pow_0 pow_succ] . {
-      rewrite pow_0.
-      Fdefn.
-    } {
-      rewrite N2Z.inj_succ.
-      rewrite Z.pow_succ_r by apply N2Z.is_nonneg.
-      rewrite <- N.add_1_l.
-      rewrite pow_succ.
-      rewrite IHn.
-      Fdefn.
-    }
-  Qed.
-
-  Lemma ZToField_eqmod : forall x y : Z, x mod m = y mod m -> ZToField x = @ZToField m y.
-    Fdefn.
-  Qed.
-
-  Lemma FieldToZ_nonzero:
-    forall x0 : F m, x0 <> 0 -> FieldToZ x0 <> 0%Z.
-  Proof.
-    intros x0 Hnz Hz.
-    rewrite <- Hz, ZToField_FieldToZ in Hnz; auto.
-  Qed.
-
-End FandZ.
-
-Section RingModuloPre.
-  Context {m:Z}.
-  Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
-  (* Substitution to prove all Compats *)
-  Ltac compat := repeat intro; subst; trivial.
-
-  Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m).
-  Proof.
-    compat.
-  Qed.
-
-  Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m).
-  Proof.
-    compat.
-  Qed.
-
-  Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m).
-  Proof.
-    compat.
-  Qed.
-
-  Instance Fopp_compat : Proper (eq==>eq) (@opp m).
-  Proof.
-    compat.
-  Qed.
-
-  Instance Finv_compat : Proper (eq==>eq) (@inv m).
-  Proof.
-    compat.
-  Qed.
-
-  Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m).
-  Proof.
-    compat.
-  Qed.
-
-  (***** Ring Theory *****)
-  Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq.
-  Proof.
-    constructor; Fdefn.
-  Qed.
-
-  Lemma F_mul_1_r:
-    forall x : F m, x * 1 = x.
-  Proof.
-    Fdefn; rewrite Z.mul_1_r; auto.
-  Qed.
-
-  Lemma F_mul_assoc:
-    forall x y z : F m, x * (y * z) = x * y * z.
-  Proof.
-    Fdefn.
-  Qed.
-
-  Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
-  Proof.
-    destruct (F_pow_spec x) as [HO HS]; intros.
-    destruct n; auto; unfold id.
-    rewrite Pre.N_pos_1plus at 1.
-    rewrite HS.
-    simpl.
-    induction p using Pos.peano_ind.
-    - simpl. rewrite HO; apply F_mul_1_r.
-    - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ F_mul_assoc x).
-      rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS.
-      f_equal.
-  Qed.
-
-  (***** Power theory *****)
-  Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m).
-  Proof.
-    constructor; apply F_pow_pow_N.
-  Qed.
-
-  (***** Division Theory *****)
-  Definition Fquotrem(a b: F m): F m * F m :=
-    let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m).
-  Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.
-  Proof.
-    constructor; intros; unfold Fquotrem, id.
-
-    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by
-      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
-
-    Fdefn; rewrite <-Z.quot_rem'; trivial.
-  Qed.
-
-  Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z.
-    intros.
-    rewrite Zmult_mod, Z_mod_same_full.
-    rewrite Z.mul_0_r, Zmod_0_l.
-    reflexivity.
-  Qed.
-
-  Lemma Z_mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->
-                                       (-x) mod m =   y  mod m.
-  Proof.
-    intros.
-    rewrite <-Z.sub_0_l.
-    rewrite Zminus_mod. rewrite H.
-    rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.
-    destruct y; auto.
-  Qed.
-
-  Lemma Z_opp_opp : forall x : Z, (-(-x)) = x.
-    destruct x; auto.
-  Qed.
-
-  Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.
-    intros.
-    apply Z_mod_opp_equiv.
-    rewrite Z_opp_opp.
-    demod; auto.
-  Qed.
-
-  (* Define a "ring morphism" between GF and Z, i.e. an equivalence
-   * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
-   *
-   * Doing this allows us to do our coefficient manipulations in Z
-   * rather than GF, because we know it's equivalent to inject the
-   * result afterward.
-   *)
-  Lemma Fring_morph:
-      ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq
-                 0%Z 1%Z Z.add    Z.mul    Z.sub    Z.opp  Z.eqb
-                 (@ZToField m).
-  Proof.
-    constructor; intros; try Fdefn; unfold id;
-      try (apply gf_eq; simpl; intuition).
-    - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity.
-    - rewrite (proj1 (Z.eqb_eq x y)); trivial.
-  Qed.
-
-  (* Redefine our division theory under the ring morphism *)
-  Lemma Fmorph_div_theory:
+  lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *;
+  try apply eqsig_eq;
+  demod.
+
+Global Instance eq_dec {m} : DecidableRel (@eq (F m)). exact _. Defined.
+
+Global Instance commutative_ring_modulo m
+  : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul.
+Proof.
+  repeat (split || intro); unwrap_F;
+    autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence].
+Qed.
+
+
+Module Zmod.
+  Lemma pow_spec {m} a : pow a 0%N = 1%F :> F m /\ forall x, pow a (1 + x)%N = mul a (pow a x).
+  Proof. change (@pow m) with (proj1_sig (@pow_with_spec m)); destruct (@pow_with_spec m); eauto. Qed.
+
+  Section FandZ.
+    Context {m:Z}.
+    Local Open Scope F_scope.
+
+    Theorem eq_FieldToZ_iff (x y : F m) : x = y <-> FieldToZ x = FieldToZ y.
+    Proof. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed.
+
+    Lemma eq_ZToField_iff : forall x y : Z, x mod m = y mod m <-> ZToField m x = ZToField m y.
+    Proof. split; unwrap_F; congruence. Qed.
+
+    
+    Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m.
+    Proof. unwrap_F; trivial. Qed.
+
+    Lemma ZToField_FieldToZ x : ZToField m (FieldToZ x) = x :> F m.
+    Proof. unwrap_F; congruence. Qed.
+
+    
+    Lemma ZToField_mod : forall x, ZToField m x = ZToField m (x mod m).
+    Proof. unwrap_F; trivial. Qed.
+
+    Lemma mod_FieldToZ : forall (x:F m),  FieldToZ x mod m = FieldToZ x.
+    Proof. unwrap_F. congruence. Qed.
+
+    Lemma FieldToZ_0 : FieldToZ (0:F m) = 0%Z.
+    Proof. unwrap_F. apply Zmod_0_l. Qed.
+
+    Lemma ZToField_small_nonzero z : (0 < z < m)%Z -> ZToField m z <> 0.
+    Proof. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed.
+
+    Lemma FieldToZ_nonzero (x:F m) : x <> 0 -> FieldToZ x <> 0%Z.
+    Proof. intros Hnz Hz. rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. Qed.
+
+    Lemma FieldToZ_range (x : F m) : 0 < m -> 0 <= x < m.
+    Proof. intros. rewrite <- mod_FieldToZ. apply Z.mod_pos_bound. trivial. Qed.
+
+    Lemma FieldToZ_nonzero_range (x : F m) : (x <> 0) -> 0 < m -> (1 <= x < m)%Z.
+    Proof.
+      unfold not; intros Hnz Hlt.
+      rewrite eq_FieldToZ_iff, FieldToZ_0 in Hnz; pose proof (FieldToZ_range x Hlt).
+      omega.
+    Qed.
+
+    Lemma ZToField_add : forall (x y : Z),
+        ZToField m (x + y) = ZToField m x + ZToField m y.
+    Proof. unwrap_F; trivial. Qed.
+
+    Lemma FieldToZ_add : forall x y : F m,
+        FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z.
+    Proof. unwrap_F; trivial. Qed.
+
+    Lemma ZToField_mul x y : ZToField m (x * y) = ZToField _ x * ZToField _ y :> F m.
+    Proof. unwrap_F. trivial. Qed.
+
+    Lemma FieldToZ_mul : forall x y : F m,
+        FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z.
+    Proof. unwrap_F; trivial. Qed.
+    
+    Lemma ZToField_sub x y : ZToField _ (x - y) = ZToField _ x - ZToField _ y :> F m.
+    Proof. unwrap_F. trivial. Qed.
+
+    Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m.
+    Proof. unwrap_F; trivial. Qed.
+
+    Lemma ZToField_pow x n : ZToField _ x ^ n = ZToField _ (x ^ (Z.of_N n) mod m) :> F m.
+    Proof.
+      intros.
+      induction n using N.peano_ind;
+        destruct (pow_spec (@ZToField m x)) as [pow_0 pow_succ] . {
+        rewrite pow_0.
+        unwrap_F; trivial.
+      } {
+        rewrite N2Z.inj_succ.
+        rewrite Z.pow_succ_r by apply N2Z.is_nonneg.
+        rewrite <- N.add_1_l.
+        rewrite pow_succ.
+        rewrite IHn.
+        unwrap_F; trivial.
+      }
+    Qed.
+
+    Lemma FieldToZ_pow : forall (x : F m) n,
+        FieldToZ (x ^ n)%F = (FieldToZ x ^ Z.of_N n mod m)%Z.
+    Proof.
+      intros.
+      symmetry.
+      induction n using N.peano_ind;
+        destruct (pow_spec x) as [pow_0 pow_succ] . {
+        rewrite pow_0, Z.pow_0_r; auto.
+      } {
+        rewrite N2Z.inj_succ.
+        rewrite Z.pow_succ_r by apply N2Z.is_nonneg.
+        rewrite <- N.add_1_l.
+        rewrite pow_succ.
+        rewrite <- Zmult_mod_idemp_r.
+        rewrite IHn.
+        apply FieldToZ_mul.
+      }
+    Qed.
+
+    Lemma square_iff (x:F m) :
+      (exists y : F m, y * y = x) <-> (exists y : Z, y * y mod m = x)%Z.
+    Proof.
+      setoid_rewrite eq_FieldToZ_iff; setoid_rewrite FieldToZ_mul; split; intro H; destruct H as [x' H].
+      - eauto.
+      - exists (ZToField _ x'); rewrite !FieldToZ_ZToField; demod; auto.
+    Qed.
+
+    (* TODO: move to ZUtil *)
+    Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.
+    Proof.
+      intros.
+      replace (x + (m - y))%Z with (m+(x-y))%Z by omega.
+      rewrite Zplus_mod.
+      rewrite Z_mod_same_full; simpl Z.add.
+      rewrite Zmod_mod.
+      reflexivity.
+    Qed.
+  End FandZ.
+
+  Section RingTacticGadgets.
+    Context (m:Z).
+
+    Definition ring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq
+      := Algebra.Ring.ring_theory_for_stdlib_tactic.
+
+    Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
+    Proof.
+      destruct (pow_spec x) as [HO HS]; intros.
+      destruct n; auto; unfold id.
+      rewrite Pre.N_pos_1plus at 1.
+      rewrite HS.
+      simpl.
+      induction p using Pos.peano_ind.
+      - simpl. rewrite HO. apply Algebra.right_identity.
+      - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ associative x).
+        rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS.
+        trivial.
+    Qed.
+
+    Lemma power_theory : power_theory 1%F (@mul m) eq id (@pow m).
+    Proof. split; apply pow_pow_N. Qed.
+
+    (***** Division Theory *****)
+    Definition quotrem(a b: F m): F m * F m :=
+      let '(q, r) := (Z.quotrem a b) in (ZToField _ q , ZToField _ r).
+    Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) quotrem.
+    Proof.
+      constructor; intros; unfold quotrem, id.
+
+      replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by
+          try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+      unwrap_F; rewrite <-Z.quot_rem'; trivial.
+    Qed.
+
+    Lemma Z_mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->
+                                           (-x) mod m =   y  mod m.
+    Proof.
+      intros.
+      rewrite <-Z.sub_0_l.
+      rewrite Zminus_mod. rewrite H.
+      rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.
+      destruct y; auto.
+    Qed.
+
+    Lemma Z_opp_opp : forall x : Z, (-(-x)) = x.
+      destruct x; auto.
+    Qed.
+
+    Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.
+      intros.
+      apply Z_mod_opp_equiv.
+      rewrite Z_opp_opp.
+      demod; auto.
+    Qed.
+
+    (* Define a "ring morphism" between GF and Z, i.e. an equivalence
+     * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
+     *
+     * Doing this allows the [ring] tactic to do coefficient
+     * manipulations in Z rather than F, because we know it's equivalent
+     * to inject the result afterward. *)
+    Lemma ring_morph: ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq
+                                 0%Z 1%Z Z.add    Z.mul    Z.sub    Z.opp  Z.eqb  (@ZToField m).
+    Proof. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed.
+
+    (* Redefine our division theory under the ring morphism *)
+    Lemma morph_div_theory:
       div_theory eq Zplus Zmult (@ZToField m) Z.quotrem.
-  Proof.
-    constructor; intros; intuition.
-    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
-      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
-
-    eq_remove_proofs; demod;
-      rewrite <- (Z.quot_rem' a b);
-      destruct a; simpl; trivial.
-  Qed.
-
-  Lemma ZToField_1 : @ZToField m 1 = 1.
-  Proof.
-    Fdefn.
-  Qed.
-End RingModuloPre.
-
-Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
-Ltac Fexp_tac t := Ncst t.
-Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
-Ltac Fpostprocess := repeat split;
-  repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] =>
-    change (exist a b (Pre.Z_mod_mod x q)) with (@ZToField q x%Z) end;
-  rewrite ?ZToField_0, ?ZToField_1.
-
-Module Type Modulus.
-  Parameter modulus : Z.
-End Modulus.
-
-(* Example of how to instantiate the ring tactic *)
-Module RingModulo (Export M : Modulus).
-  Definition ring_theory_modulo := @Fring_theory modulus.
-  Definition ring_morph_modulo := @Fring_morph modulus.
-  Definition morph_div_theory_modulo := @Fmorph_div_theory modulus.
-  Definition power_theory_modulo := @Fpower_theory modulus.
-
-  Add Ring GFring_Z : ring_theory_modulo
-    (morphism ring_morph_modulo,
-     constants [Fconstant],
-     div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]).
-End RingModulo.
-
-Section VariousModulo.
-  Context {m:Z}.
-
-  Add Ring GFring_Z : (@Fring_theory m)
-    (morphism (@Fring_morph m),
-     constants [Fconstant],
-     div (@Fmorph_div_theory m),
-     power_tac (@Fpower_theory m) [Fexp_tac]).
-
-  Lemma F_mul_0_l : forall x : F m, 0 * x = 0.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_0_r : forall x : F m, x * 0 = 0.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
-    intros; intuition; subst.
-    assert (0 * b = 0) by ring; intuition.
-  Qed.
-
-  Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
-    intros; intuition; subst.
-    assert (a * 0 = 0) by ring; intuition.
-  Qed.
-
-  Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N ->
-    (x ^ z) * (y ^ z) = (x * y) ^ z.
-  Proof.
-    intros.
-    replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
-    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | |
-      replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
-    intros z' z'_nonneg IHz'.
-    rewrite Z2N.inj_succ by auto.
-    rewrite <-N.add_1_l.
-    rewrite !(proj2 (@F_pow_spec m _) _).
-    rewrite <- IHz'.
-    ring.
-  Qed.
-
-  Lemma F_opp_0 : opp (0 : F m) = 0%F.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y.
-  Proof.
-    split; intro; subst; ring.
-  Qed.
-
-  Lemma F_opp_involutive : forall x : F m, opp (opp x) = x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_square_opp : forall x : F m, (opp x ^ 2 = x ^ 2)%F.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_opp_r : forall x y : F m, (x * opp y = opp (x * y))%F.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_opp_l : forall x y : F m, (opp x * y = opp (x * y))%F.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_opp_both : forall x y : F m, (opp x * opp y = x * y)%F.
-    intros; ring.
-  Qed.
-
-  Lemma F_add_0_r : forall x : F m, (x + 0)%F = x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_add_0_l : forall x : F m, (0 + x)%F = x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z.
-  Proof.
-    intros ? ? ? A.
-    replace y with (y + x - x) by ring.
-    rewrite A; ring.
-  Qed.
-
-  Lemma F_add_reg_l : forall x y z : F m, x + y = x + z -> y = z.
-  Proof.
-    intros ? ? ? A.
-    replace y with (x + y - x) by ring.
-    rewrite A; ring.
-  Qed.
-
-  Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x.
-  Proof.
-    intros; ring.
-  Qed.
-
-  Lemma F_ZToField_m : ZToField m = @ZToField m 0.
-  Proof.
-    Fdefn.
-    rewrite Zmod_0_l.
-    apply Z_mod_same_full.
-  Qed.
-
-  Lemma F_sub_m_l : forall x : F m, opp x = ZToField m - x.
-  Proof.
-    rewrite F_ZToField_m.
-    symmetry.
-    apply F_sub_0_l.
-  Qed.
-
-  Lemma opp_ZToField : forall x : Z, opp (ZToField x) = @ZToField m (m - x).
-  Proof.
-    Fdefn.
-    rewrite Zminus_mod, Z_mod_same_full, (Z.sub_0_l (x mod m)); reflexivity.
-  Qed.
-
-  Lemma F_pow_2_r : forall x : F m, x^2 = x*x.
-  Proof.
-    intros. ring.
-  Qed.
-
-  Lemma F_pow_3_r : forall x : F m, x^3 = x*x*x.
-  Proof.
-    intros. ring.
-  Qed.
-
-  Lemma F_pow_add : forall (x : F m) k j, x ^ j * x ^ k = x ^ (j + k).
-  Proof.
-    intros.
-    destruct (F_pow_spec x) as [exp_zero exp_succ].
-    induction j using N.peano_ind.
-    + rewrite exp_zero.
-      ring_simplify; eauto.
-    +
-    rewrite N.add_succ_l.
-    do 2 rewrite <- N.add_1_l.
-    do 2 rewrite exp_succ by apply N.neq_succ_0.
-    rewrite <- IHj.
-    ring.
-  Qed.
-
-  Lemma F_pow_compose : forall (x : F m) k j, (x ^ j) ^ k = x ^ (k * j).
-  Proof.
-    intros.
-    induction k using N.peano_ind; [rewrite Nmult_0_l; ring | ].
-    rewrite Nmult_Sn_m.
-    rewrite <- F_pow_add.
-    rewrite <- IHk.
-    rewrite <- N.add_1_l.
-    rewrite (proj2 (F_pow_spec _)).
-    ring.
-  Qed.
-
-  Lemma F_sub_add_swap : forall w x y z : F m, w - x = y - z <-> w + z = y + x.
-  Proof.
-    split; intro A;
-      [ replace w with (w - x + x) by ring
-      | replace w with (w + z - z) by ring ]; rewrite A; ring.
-  Qed.
-
-  Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x.
-
-  Lemma square_Zmod_F : forall (a : F m), isSquare a <->
-    (exists b : Z, ((b * b) mod m)%Z = a).
-  Proof.
-    split; intro A; destruct A as [sqrt_a sqrt_a_id]. {
-      exists sqrt_a.
-      rewrite <- FieldToZ_mul.
-      apply F_eq.
-      ring_simplify; auto.
-    } {
-      exists (ZToField sqrt_a).
-      rewrite ZToField_pow.
-      replace (Z.of_N 2) with 2%Z by auto.
-      rewrite Z.pow_2_r.
-      rewrite sqrt_a_id.
-      apply ZToField_FieldToZ.
-    }
-  Qed.
-
-  Lemma FieldToZ_range : forall x : F m, 0 < m -> 0 <= x < m.
-  Proof.
-    intros.
-    rewrite <- mod_FieldToZ.
-    apply Z.mod_pos_bound.
-    omega.
-  Qed.
-
-  Lemma FieldToZ_nonzero_range : forall x : F m, (x <> 0) -> 0 < m ->
-    (1 <= x < m)%Z.
-  Proof.
-    intros.
-    pose proof (FieldToZ_range x).
-    unfold not in *.
-    rewrite F_eq in H.
-    replace (FieldToZ 0) with 0%Z in H by auto.
-    omega.
-  Qed.
-
-  Lemma F_mul_comm : forall x y : F m, x*y = y*x.
-    intros; ring.
-  Qed.
-
-  Lemma Fq_sub_eq : forall x y a b : F m, a = b -> x-a = y-b -> x = y.
-  Proof.
-    intros x y a b Hab Hxayb; subst.
-    replace x with ((x - b) + b) by ring.
-    replace y with ((y - b) + b) by ring.
-    rewrite Hxayb; ring.
-  Qed.
-
-  Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z.
-  Proof.
-    intros.
-    rewrite FieldToZ_opp.
-    rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega.
-    rewrite mod_FieldToZ.
-    replace 0%Z with (@FieldToZ m 0) by auto.
-    intro false_eq.
-    rewrite <-F_eq in false_eq.
-    congruence.
-  Qed.
-
-End VariousModulo.
+    Proof.
+      split; intros.
+      replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
+        try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+      unwrap_F; rewrite <- (Z.quot_rem' a b); trivial.
+    Qed.
+
+  End RingTacticGadgets.
+
+  Ltac is_constant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
+  Ltac is_pow_constant t := Ncst t.
+
+  Module Type Modulus. Parameter modulus : Z. End Modulus.
+
+  (* Example of how to instantiate the ring tactic *)
+  Module RingModulo (Export M : Modulus).
+    Add Ring _theory : (ring_theory modulus)
+                         (morphism (ring_morph modulus),
+                          constants [is_constant],
+                          div (morph_div_theory modulus),
+                          power_tac (power_theory modulus) [is_pow_constant]).
+
+    Example ring_modulo_example : forall x y z, x*z + z*y = z*(x+y).
+    Proof. intros. ring. Qed.
+  End RingModulo.
+
+  Section VariousModulo.
+    Context {m:Z}.
+    Local Open Scope F_scope.
+
+    Add Ring _theory : (ring_theory m)
+                         (morphism (ring_morph m),
+                          constants [is_constant],
+                          div (morph_div_theory m),
+                          power_tac (power_theory m) [is_pow_constant]).
+
+    Lemma mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
+    Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed.
+
+    Lemma mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
+    Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed.
+  End VariousModulo.
+
+  Section Pow.
+    Context {m:Z}.
+    Add Ring _theory' : (ring_theory m)
+                          (morphism (ring_morph m),
+                           constants [is_constant],
+                           div (morph_div_theory m),
+                           power_tac (power_theory m) [is_pow_constant]).
+    Local Open Scope F_scope.
+
+    Import Algebra.ScalarMult.
+    Global Instance pow_is_scalarmult
+      : is_scalarmult (G:=F m) (eq:=eq) (add:=mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)).
+    Proof.
+      split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l;
+        match goal with
+        | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto]
+        | |- Proper _ _ => solve_proper
+        end.
+    Qed.
+
+    (* TODO: move this somewhere? *)
+    Create HintDb nat2N discriminated.
+    Hint Rewrite Nat2N.inj_iff
+         (eq_refl _ : (0%N = N.of_nat 0))
+         (eq_refl _ : (1%N = N.of_nat 1))
+         (eq_refl _ : (2%N = N.of_nat 2))
+         (eq_refl _ : (3%N = N.of_nat 3))
+      : nat2N.
+    Hint Rewrite <- Nat2N.inj_double Nat2N.inj_succ_double Nat2N.inj_succ
+         Nat2N.inj_add Nat2N.inj_mul Nat2N.inj_sub Nat2N.inj_pred
+         Nat2N.inj_div2 Nat2N.inj_max Nat2N.inj_min Nat2N.id
+      : nat2N.
+
+    Ltac pow_to_scalarmult_ref :=
+      repeat (autorewrite with nat2N;
+              match goal with
+              | |- context [ (_^?n)%F ] =>
+                rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n;
+                let m := fresh n in intro m
+              | |- context [ (_^N.of_nat ?n)%F ] =>
+                let rw := constr:(scalarmult_ext(zero:=ZToField m 1) n) in
+                setoid_rewrite rw (* rewriting moduloa reduction *)
+              end).
+
+    Lemma pow_0_r (x:F m) : x^0 = 1.
+    Proof. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed.
+
+    Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b.
+    Proof. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed.
+
+    Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m.
+    Proof. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed.
+
+    Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b).
+    Proof. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed.
+
+    Lemma pow_1_r (x:F m) : x^1 = x.
+    Proof. pow_to_scalarmult_ref; simpl; ring. Qed.
+
+    Lemma pow_2_r (x:F m) : x^2 = x*x.
+    Proof. pow_to_scalarmult_ref; simpl; ring. Qed.
+
+    Lemma pow_3_r (x:F m) : x^3 = x*x*x.
+    Proof. pow_to_scalarmult_ref; simpl; ring. Qed.
+  End Pow.
+End Zmod.
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 4fd881e1e..f80ce05f8 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -37,9 +37,9 @@ Section ModularBaseSystem.
    from_list (sub [[modulus_multiple]] [[us]] [[vs]])
    (length_sub length_to_list length_to_list length_to_list).
 
-  Definition zero : digits := encode (ZToField 0).
+  Definition zero : digits := encode (ZToField _ 0).
 
-  Definition one : digits := encode (ZToField 1).
+  Definition one : digits := encode (ZToField _ 1).
 
   (* Placeholder *)
   Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)).
diff --git a/src/ModularArithmetic/ModularBaseSystemField.v b/src/ModularArithmetic/ModularBaseSystemField.v
index f5bedd644..b26ca027d 100644
--- a/src/ModularArithmetic/ModularBaseSystemField.v
+++ b/src/ModularArithmetic/ModularBaseSystemField.v
@@ -11,6 +11,7 @@ Local Open Scope Z_scope.
 Section ModularBaseSystemField.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
+  Local Existing Instance prime_modulus.
   Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
   Local Notation digits := (tuple Z (length limb_widths)).
 
@@ -35,17 +36,13 @@ Section ModularBaseSystemField.
     apply carry_mul_rep; apply decode_rep.
   Qed.
 
-  Lemma zero_neq_one : eq zero one -> False.
-  Proof.
-   cbv [eq zero one]. erewrite !encode_rep. intro A.
-   eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)).
-   congruence.
-  Qed.
+  Lemma _zero_neq_one : not (eq zero one).
+  Proof. cbv [eq zero one]. erewrite !encode_rep; apply zero_neq_one. Qed.
 
   Lemma modular_base_system_field :
     @field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div.
   Proof.
-    eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo  (prime_q := prime_modulus))).
+    eapply (Field.isomorphism_to_subfield_field (phi := decode)).
     Grab Existential Variables.
     + intros; eapply encode_rep.
     + intros; eapply encode_rep.
@@ -55,9 +52,7 @@ Section ModularBaseSystemField.
     + intros; eapply sub_decode.
     + intros; eapply add_decode.
     + intros; eapply encode_rep.
-    + cbv [eq zero one]. erewrite !encode_rep. intro A.
-      eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)).
-      congruence.
+    + eapply _zero_neq_one.
     + trivial.
     + repeat intro. cbv [div]. congruence.
     + repeat intro. cbv [inv]. congruence.
@@ -65,7 +60,6 @@ Section ModularBaseSystemField.
     + repeat intro. cbv [eq]. erewrite !sub_decode. congruence.
     + repeat intro. cbv [eq]. erewrite !add_decode. congruence.
     + repeat intro. cbv [opp]. congruence.
-    + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
   Qed.
 
 End ModularBaseSystemField.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
index c556427b9..f8d78a438 100644
--- a/src/ModularArithmetic/ModularBaseSystemList.v
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -16,7 +16,7 @@ Section Defs.
   Local Notation base := (base_from_limb_widths limb_widths).
   Local Notation "u [ i ]" := (nth_default 0 u i).
 
-  Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
+  Definition decode (us : digits) : F modulus := ZToField _ (BaseSystem.decode base us).
 
   Definition encode (x : F modulus) := encodeZ limb_widths x.
 
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index d740cca17..720fa8ea1 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -21,6 +21,8 @@ Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z_scope.
 
 Local Opaque add_to_nth carry_simple.
+Local Arguments ZToField {_} _.
+Import ModularArithmeticTheorems.Zmod PrimeFieldTheorems.Zmod.
 
 Section PseudoMersenneProofs.
   Context `{prm :PseudoMersenneBaseParams}.
@@ -232,7 +234,7 @@ Section PseudoMersenneProofs.
     rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep.
     rewrite ZToField_sub, ZToField_add, ZToField_mod.
     apply Fdecode_decode_mod in mm_spec; cbv [BaseSystem.decode] in *.
-    rewrite mm_spec, F_add_0_l.
+    rewrite mm_spec. rewrite Algebra.left_identity.
     f_equal; assumption.
   Qed.
 
@@ -297,11 +299,11 @@ Section CarryProofs.
     specialize_by eauto.
     cbv [ModularBaseSystemList.carry].
     break_if; subst; eauto.
-    apply F_eq.
+    apply eq_ZToField_iff.
     rewrite to_list_from_list.
     apply carry_decode_eq_reduce. auto.
     cbv [ModularBaseSystemList.decode].
-    apply ZToField_eqmod.
+    apply eq_ZToField_iff.
     rewrite to_list_from_list, carry_simple_decode_eq; try omega; distr_length; auto.
   Qed.
   Hint Resolve carry_rep.
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index 8566d30ab..7320b16bf 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -119,8 +119,8 @@ Program Definition inv_impl {m : BinNums.Z} :
     forall a : {z : BinNums.Z | z = z mod m},
     a <> exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) ->
     exist (fun z : BinNums.Z => z = z mod m)
-      ((proj1_sig a * proj1_sig (inv0 a)) mod m)
-      (Z_mod_mod (proj1_sig a * proj1_sig (inv0 a)) m) =
+      ((proj1_sig (inv0 a) * proj1_sig a) mod m)
+      (Z_mod_mod (proj1_sig (inv0 a) * proj1_sig a) m) =
     exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}
      := mod_inv_sig.
 Next Obligation.
@@ -130,7 +130,7 @@ Next Obligation.
   assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega).
   assert (Ha:a mod m<>0) by (intro; apply Ha', exist_reduced_eq; congruence).
   cbv [proj1_sig mod_inv_sig].
-  transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; congruence|].
+  transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; f_equal; ring|].
   rewrite !powmod_Zpow_mod.
   rewrite Z2N.id by assumption.
   rewrite Zmult_mod_idemp_r.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 8d47e36ed..c97bde495 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -10,568 +10,171 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.Algebra.
+Import Crypto.ModularArithmetic.ModularArithmeticTheorems.Zmod.
 
 Existing Class prime.
 
-Lemma F_inv_spec : forall {m}, inv 0%F = (0%F : F m)
-      /\ (prime m -> forall a0 : F m, a0 <> 0%F -> (a0 * inv a0)%F = 1%F).
-Proof.
-  intros m.
-  pose (@inv_with_spec m) as H.
-  change (@inv m) with (proj1_sig H).
-  destruct H; eauto.
-Qed.
-
-Section FieldModuloPre.
-  Context {q:Z} {prime_q:prime q}.
-  Local Open Scope F_scope.
-
-  Lemma Fq_1_neq_0 : (1:F q) <> (0:F q).
-  Proof.
-    pose proof prime_ge_2 q _.
-    rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence.
-  Qed.
-
-  Lemma F_mul_inv_r : forall x : F q, x <> 0 -> x * inv x = 1.
-  Proof.
-    intros.
-    edestruct @F_inv_spec; eauto.
-  Qed.
-
-  Lemma F_mul_inv_l : forall x : F q, x <> 0 -> inv x * x = 1.
-  Proof.
-    intros.
-    edestruct @F_inv_spec as [Ha Hb]; eauto.
-    erewrite <-Hb; eauto.
-    Fdefn.
-  Qed.
-
-  (* Add an abstract field (without modifiers) *)
-  Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq.
-  Proof.
-    constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l.
-  Qed.
-
-  Global Instance field_modulo : @Algebra.field (F q) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul inv div.
-  Proof.
-    constructor; try solve_proper.
-    - apply commutative_ring_modulo.
-    - split. auto using F_mul_inv_l.
-    - split. auto using Fq_1_neq_0.
-  Qed.
-End FieldModuloPre.
-
-Module Type PrimeModulus.
-  Parameter modulus : Z.
-  Parameter prime_modulus : prime modulus.
-End PrimeModulus.
-
-Module FieldModulo (Import M : PrimeModulus).
-  (* Add our field with all the fixin's *)
-  Module Import RingM := RingModulo M.
-  Definition field_theory_modulo := @Ffield_theory modulus prime_modulus.
-  Add Field Ffield_Z : field_theory_modulo
-    (morphism ring_morph_modulo,
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess],
-     constants [Fconstant],
-     div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]).
-End FieldModulo.
-
-Section VariousModPrime.
-  Context {q:Z} {prime_q:prime q}.
-  Local Open Scope F_scope.
-  Add Field Ffield_Z : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
-
-  Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y.
-  Proof.
-    intros ? ? ? z_nonzero mul_z_eq.
-    assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity).
-    replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial).
-    replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial).
-    rewrite F_mul_inv_r in H by assumption.
-    replace (x * 1) with x in H by field.
-    replace (y * 1) with y in H by field.
-    trivial.
-  Qed.
-
-  Lemma Fq_mul_eq_l : forall x y z : F q, z <> 0 -> z * x = z * y -> x = y.
-  Proof.
-    intros ? ? ? Hz Heq.
-    apply (Fq_mul_eq _ _ z); auto.
-    apply (Fq_sub_eq _ _ _ _ Heq); ring.
-  Qed.
-
-  Lemma Fq_inv_unique' : forall
-      inv1 (inv1ok: inv1 0 = 0 /\ forall x : F q, x <> 0 ->  x * inv1 x = 1)
-      inv2 (inv2ok: inv2 0 = 0 /\ forall x : F q, x <> 0 ->  x * inv2 x = 1),
-      forall x, inv1 x = inv2 x.
-  Proof.
-    intros inv1 [inv1_0 inv1_x] inv2 [inv2_0 inv2_x] x.
-    destruct (F_eq_dec x 0) as [H|H]; [congruence|].
-    apply (Fq_mul_eq_l _ _ x H). rewrite inv1_x, inv2_x; trivial.
-  Qed.
-
-  Lemma Fq_inv_unique : forall
-      inv' (inv'ok: inv' 0 = 0 /\ forall x : F q, x <> 0 -> x * inv' x = 1),
-      forall x, inv x = inv' x.
-  Proof.
-    intros ? [? ?] ?.
-    pose proof (@F_inv_spec q) as [? ?].
-    eauto using Fq_inv_unique'.
-  Qed.
-
-  Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0.
-    intros.
-    assert (Z := F_eq_dec a 0); destruct Z.
-
-    - left; intuition.
-
-    - assert (a * b / a = 0) by
-        ( rewrite H; field; intuition ).
-
-      replace (a*b/a) with (b) in H0 by (field; trivial).
-      right; intuition.
-  Qed.
-
-  Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0.
-    intros; intuition; subst.
-    apply Fq_mul_zero_why in H1.
-    destruct H1; subst; intuition.
-  Qed.
-  Hint Resolve Fq_mul_nonzero_nonzero.
-
-  Lemma Fq_pow_zero : forall (p: N), p <> 0%N -> (0^p = @ZToField q 0)%F.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intuition.
-    - intro H. apply F_mul_0_l.
-  Qed.
-
-  Lemma Fq_root_zero : forall (x: F q) (p: N), x^p = 0 -> x = 0.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intros; destruct Fq_1_neq_0; auto.
-    - intro H; destruct (Fq_mul_zero_why x (x^p) H); auto.
-  Qed.
-
-  Lemma Fq_root_nonzero : forall (x:F q) p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intuition.
-    - destruct (N.eq_dec p 0); intro H; intros; subst.
-      + rewrite (proj1 (@F_pow_spec q _)) in H; replace (x*1) with (x) in H by ring; trivial.
-      + apply IHp; auto. intro Hz; rewrite Hz in *. apply H, F_mul_0_r.
-  Qed.
-
-  Lemma Fq_pow_nonzero : forall (x : F q) p, x <> 0 -> x^p <> 0.
-  Proof.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intuition. auto using Fq_1_neq_0.
-    - intros H Hc. destruct (Fq_mul_zero_why _ _ Hc).
-      + intuition.
-      + apply IHp; auto.
-  Qed.
-
-  Lemma F_inv_0 : inv 0 = (0 : F q).
-  Proof.
-    destruct (@F_inv_spec q); auto.
-  Qed.
-
-  Definition inv_fermat (x:F q) : F q := x ^ Z.to_N (q - 2)%Z.
-  Lemma Fq_inv_fermat: 2 < q -> forall x : F q, inv x = x ^ Z.to_N (q - 2)%Z.
-  Proof.
-    intros.
-    erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat.
-    { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto.
-      rewrite Fq_pow_zero. reflexivity. intro.
-      assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. }
-    { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf.
-      { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. }
-      specialize (Hf H1); clear H1.
-      rewrite <-(ZToField_FieldToZ x).
-      rewrite ZToField_pow.
-      replace (Z.of_N (Z.to_N (q - 2))) with (q-2)%Z by (rewrite Z2N.id ; omega).
-      rewrite <-ZToField_mul.
-      apply ZToField_eqmod.
-      rewrite Hf, Zmod_small by omega; reflexivity.
-    }
-  Qed.
-  Lemma Fq_inv_fermat_correct : 2 < q -> forall x : F q, inv_fermat x = inv x.
-  Proof.
-    unfold inv_fermat; intros. rewrite Fq_inv_fermat; auto.
-  Qed.
-
-  Let inv_fermat_powmod (x:Z) : Z := powmod q x (Z.to_N (q-2)).
-  Lemma FieldToZ_inv_efficient : 2 < q ->
-                                 forall x : F q, FieldToZ (inv x) = inv_fermat_powmod x.
-  Proof.
-    unfold inv_fermat_powmod; intros.
-    rewrite Fq_inv_fermat, powmod_Zpow_mod, <-FieldToZ_pow_Zpow_mod; auto.
-  Qed.
+Module Zmod.
+  Section Field.
+    Context (q:Z) {prime_q:prime q}.
+    Lemma inv_spec : inv 0%F = (0%F : F q) 
+                     /\ (prime q -> forall x : F q, x <> 0%F -> (inv x * x)%F = 1%F).
+    Proof. change (@inv q) with (proj1_sig (@inv_with_spec q)); destruct (@inv_with_spec q); eauto. Qed.
+
+    Lemma inv_0 : inv 0 = ZToField q 0. Proof. destruct inv_spec; auto. Qed.
+    Lemma inv_nonzero (x:F q) : (x <> 0 -> inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed.
+
+    Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F opp add sub mul inv div.
+    Proof.
+      repeat match goal with
+             | _ => solve [ solve_proper
+                          | apply commutative_ring_modulo
+                          | apply inv_nonzero
+                          | cbv [not]; pose proof prime_ge_2 q prime_q;
+                            rewrite Zmod.eq_FieldToZ_iff, !Zmod.FieldToZ_ZToField, !Zmod_small; omega ]
+             | _ => split
+             end.
+    Qed.
 
-  Lemma F_minus_swap : forall x y : F q, x - y = 0 -> y - x = 0.
-  Proof.
-    intros ? ? eq_zero.
-    replace x with (x - y + y); try ring.
-    rewrite eq_zero.
-    ring.
-  Qed.
+    Definition field_theory : field_theory 0%F 1%F add mul sub opp div inv eq
+      := Algebra.Field.field_theory_for_stdlib_tactic.
+  End Field.
+
+  (** A field tactic hook that can be imported *)
+  Module Type PrimeModulus.
+    Parameter modulus : Z.
+    Parameter prime_modulus : prime modulus.
+  End PrimeModulus.
+  Module FieldModulo (Export M : PrimeModulus).
+    Module Import RingM := RingModulo M.
+    Add Field _field : (field_theory modulus)
+                         (morphism (ring_morph modulus),
+                          constants [is_constant],
+                          div (morph_div_theory modulus),
+                          power_tac (power_theory modulus) [is_pow_constant]).
+  End FieldModulo.
+
+  Section NumberThoery.
+    Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}.
+    Local Open Scope F_scope.
+    Add Field _field : (field_theory q)
+                         (morphism (ring_morph q),
+                          constants [is_constant],
+                          div (morph_div_theory q),
+                          power_tac (power_theory q) [is_pow_constant]).
+
+    Lemma FieldToZ_1 : @FieldToZ q 1 = 1%Z.
+    Proof. simpl. rewrite Zmod_small; omega. Qed.
+
+    Lemma Fq_inv_fermat (x:F q) : inv x = x ^ Z.to_N (q - 2)%Z.
+    Proof.
+      destruct (dec (x = 0%F)) as [?|Hnz]; [subst x; rewrite inv_0|].
+      { admit. }
+      erewrite <-Algebra.Field.inv_unique; try reflexivity.
+      rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega.
+      apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial.
+    Qed.
 
-  Lemma Fq_square_mul : forall x y z : F q, (y <> 0) ->
-    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
-  Proof.
-    intros ? ? ? y_nonzero A.
-    exists (x / y).
-    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial).
-    assert (y ^ 2 <> 0) as y2_nonzero by (
-      change (2%N) with (1+(1+0))%N;
-      rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _));
-      auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0).
-    rewrite (Fq_mul_eq _ z (y ^ 2)); auto.
-    rewrite <- A.
-    field; trivial.
-  Qed.
+    (* TODO: move to number thoery util *)
+    Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z.
+    Proof.
+      rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1.
+      apply Z_div_mod_eq; reflexivity.
+    Qed.
+    
+    Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) :
+      (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a).
+    Proof.
+      pose proof FieldToZ_nonzero_range a; pose proof (odd_as_div q).
+      specialize_by ltac:(destruct (Z.prime_odd_or_2 _ prime_q); try omega; trivial).
+      rewrite eq_FieldToZ_iff, !FieldToZ_pow, !FieldToZ_1, !Z2N.id by omega.
+      rewrite square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity.
+    Qed.
 
-  Lemma Fq_square_mul_sub : forall x y z : F q,
-    0 = z * y ^ 2 - x ^ 2 -> (exists sqrt_z, sqrt_z ^ 2 = z) \/ x = 0.
-  Proof.
-    intros ? ? ? eq_zero_sub.
-    destruct (F_eq_dec y 0). {
+    Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x).
+    Proof.
+      destruct (dec (x = 0)).
+      { left. abstract (exists 0; subst; ring). }
+      { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. }
+    Defined.
+  End NumberThoery.
+
+  Section SquareRootsPrime5Mod8.
+    Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
+
+    (* This is always true, but easier to check by computation than to prove *)
+    Context (sqrt_minus1_valid : ((ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F).
+    Local Open Scope F_scope.
+    Add Field _field2 : (field_theory q)
+                          (morphism (ring_morph q),
+                           constants [is_constant],
+                           div (morph_div_theory q),
+                           power_tac (power_theory q) [is_pow_constant]).
+
+    Let sqrt_minus1 : F q :=  ZToField _ 2 ^ Z.to_N (q / 4).
+
+    Lemma two_lt_q_5mod8 : 2 < q.
+    Proof.
+      pose proof (prime_ge_2 q _) as two_le_q.
+      apply Zle_lt_or_eq in two_le_q.
+      destruct two_le_q; auto.
       subst_max.
-      rewrite Fq_pow_zero in eq_zero_sub by congruence.
-      rewrite F_mul_0_r in eq_zero_sub.
-      assert (x ^ 2 = 0 - x ^ 2 + x ^ 2) as minus_plus_x2 by (rewrite <- eq_zero_sub; ring).
-      assert (x ^ 2 = 0) as x2_zero by (rewrite minus_plus_x2; ring).
-      apply Fq_root_zero in x2_zero.
-      right; auto.
-    } {
-      left.
-      eapply Fq_square_mul; eauto.
-      instantiate (1 := x).
-      assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by
-        (rewrite <- eq_zero_sub; ring).
-      rewrite plus_minus_x2; ring.
-    }
-  Qed.
-
-  Lemma F_div_mul : forall x y z : F q, y <> 0 -> (z = (x / y) <-> z * y = x).
-  Proof.
-    split; intros; subst; field.
-  Qed.
-
-  Lemma F_div_1_r : forall x : F q, (x/1)%F = x.
-  Proof.
-    intros; field. (* TODO: Warning: Collision between bound variables ... *)
-  Qed.
-
-  Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F.
-  Proof.
-    intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field.
-  Qed.
-
-  Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0).
-  Proof.
-    split; intro A.
-    + pose proof (F_opp_spec x) as opp_spec.
-      rewrite <- A in opp_spec.
-      replace (x + x) with (ZToField 2 * x) in opp_spec by ring.
-      apply Fq_mul_zero_why in opp_spec.
-      destruct opp_spec as [eq_2_0 | ?]; auto.
-      apply F_eq in eq_2_0.
-      rewrite FieldToZ_ZToField in eq_2_0.
-      replace (FieldToZ 0) with 0%Z in eq_2_0 by auto.
-      replace (2 mod q) with 2 in eq_2_0; try discriminate.
-      symmetry; apply Z.mod_small; omega.
-    + subst.
-      rewrite <- (F_opp_spec 0) at 1.
-      ring.
-  Qed.
-
-  Lemma euler_criterion_F : forall (a : F q) (q_odd : 2 < q) (a_nonzero : a <> 0),
-    (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a.
-  Proof.
-    (*pose proof q_odd.*)
-    split; intros A. {
-      apply square_Zmod_F; auto.
-      eapply euler_criterion; omega || auto.
-      + apply div2_p_1mod4; auto; omega.
-      + pose proof (FieldToZ_nonzero_range a a_nonzero); omega.
-      + replace (q / 2)%Z with (Z.of_N (Z.to_N (q / 2)))
-          by (apply Z2N.id; apply Z.div_pos; prime_bound).
-        rewrite FieldToZ_pow_Zpow_mod by omega.
-        rewrite A.
-        replace (FieldToZ 1) with (1 mod q) by auto.
-        apply Z.mod_1_l; omega.
-    } {
-      apply F_eq.
-      rewrite <- FieldToZ_pow_Zpow_mod by omega.
-      rewrite Z2N.id by (apply Z.div_pos; omega).
-      replace (FieldToZ 1) with 1%Z
-        by (rewrite FieldToZ_ZToField at 1; symmetry; apply Zmod_1_l; omega).
-      apply euler_criterion; try prime_bound; auto.
-      + apply div2_p_1mod4; auto; omega.
-      + pose proof (FieldToZ_nonzero_range a a_nonzero); omega.
-      + apply square_Zmod_F; auto.
-    }
-  Qed.
-
-  Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q),
-    if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1))
-    then (isSquare a) else (forall b, b ^ 2 <> a).
-  Proof.
-    unfold orb; intros.
-    rewrite <- if_F_eq_dec_if_F_eqb.
-    do 2 break_if; try congruence.
-    + subst; exists 0; apply Fq_pow_zero; congruence.
-    + unfold isSquare; apply F_eqb_eq in Heqb; apply euler_criterion_F; eauto.
-    + intros b b_id.
-      apply F_eqb_neq in Heqb.
-      assert (isSquare a) as a_square by (eexists; eauto).
-      apply euler_criterion_F in a_square; auto.
-  Qed.
-
-  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
-    if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1)
-    then (isSquare a) else (forall b, b ^ 2 <> a).
-  Proof.
-    intros.
-    pose proof (euler_criterion_if' a q_odd) as H.
-    unfold F_eqb in H.
-    rewrite !FieldToZ_ZToField, !@FieldToZ_pow_efficient, !Zmod_small in H by omega; assumption.
-  Qed.
-
-  Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
-  Proof.
-    intros ? ? squares_eq.
-    remember (y - x) as z.
-    replace y with (x + z) in * by (rewrite Heqz; ring).
-    replace (x ^ 2) with (0 + x ^ 2) in squares_eq by ring.
-    replace ((x + z) ^ 2) with (z * (x + (x + z)) + x ^ 2) in squares_eq by ring.
-    apply F_add_reg_r in squares_eq.
-    apply Fq_mul_zero_why in squares_eq.
-    destruct squares_eq as [? | z_2x_0]; [ left; subst; ring | right ].
-    pose proof (F_opp_spec x) as opp_spec.
-    rewrite <- z_2x_0 in opp_spec.
-    apply F_add_reg_l in opp_spec; auto.
-  Qed.
-
-  Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq.
-  Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops.
-  Proof.
-    econstructor; eauto with typeclass_instances;
-      unfold R2, equality, eq_notation, addition, add_notation, one, one_notation,
-      multiplication, mul_notation, zero, zero_notation, subtraction,
-      sub_notation, opposite, opp_notation; intros; ring.
+      discriminate.
     Qed.
 
-  Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring.
-  Proof.
-    repeat intro. apply F_mul_comm.
-  Qed.
-
-  Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring.
-  Proof.
-    econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0.
-  Qed.
-
-  Lemma add_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
-    : x * y + z = (x + (z * (inv y))) * y.
-  Proof. field. Qed.
-
-  Lemma sub_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
-    : x * y - z = (x - (z * (inv y))) * y.
-  Proof. field. Qed.
-
-  Lemma add_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
-    : y + z = (1 + (z * (inv y))) * y.
-  Proof. field. Qed.
-
-  Lemma sub_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
-    : y - z = (1 - (z * (inv y))) * y.
-  Proof. field. Qed.
-End VariousModPrime.
-
-Section SquareRootsPrime5Mod8.
-  Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
-
-  (* This is always true, but easier to check by computation than to prove *)
-  Context (sqrt_minus1_valid : ((ZToField 2 ^ Z.to_N (q / 4)) ^ 2 = @opp q 1)%F).
-
-  Local Open Scope F_scope.
-  Add Field Ffield_8mod5 : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
-
-  (* This is only the square root of -1 if q mod 8 is 3 or 5 *)
-  Definition sqrt_minus1 : F q :=  ZToField 2 ^ Z.to_N (q / 4).
-
-  Lemma two_lt_q_5mod8 : 2 < q.
-  Proof.
-    pose proof (prime_ge_2 q _) as two_le_q.
-    apply Zle_lt_or_eq in two_le_q.
-    destruct two_le_q; auto.
-    subst_max.
-    discriminate.
-  Qed.
-
-  (* square root mod q relies on the fact that q is 5 mod 8 *)
-  Definition sqrt_mod_q (a : F q) :=
-    let b := a ^ Z.to_N (q / 8 + 1) in
-    (match (F_eq_dec (b ^ 2) a) with
-    | left A => b
-    | right A => (sqrt_minus1 * b)%F
-    end).
-
-  Lemma eq_b4_a2 : forall x : F q, isSquare x ->
-    ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2.
-  Proof.
-    intros.
-    destruct (F_eq_dec x 0). {
-      subst.
-      repeat rewrite Fq_pow_zero; try (intuition; discriminate).
-      intro false_eq.
-      assert (0 <= q / 8)%Z by zero_bounds.
-      assert (0 < q / 8 + 1) by omega.
-      replace 0%N with (Z.to_N 0) in * by auto.
-      apply Z2N.inj in false_eq; omega.
-    } {
-      rewrite F_pow_compose.
-      replace (2 * 2)%N with 4%N by auto.
-      rewrite F_pow_compose.
-      replace (4 * Z.to_N (q / 8 + 1))%N with (Z.to_N (q / 2 + 2))%N.
+    Definition sqrt_5mod8 (a : F q) : F q :=
+      let b := a ^ Z.to_N (q / 8 + 1) in
+      if dec (b ^ 2 = a)
+      then b
+      else sqrt_minus1 * b.
+    
+    Lemma eq_b4_a2 (x : F q) (Hex:exists y, y*y = x) :
+      ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2.
+    Proof.
+      pose proof two_lt_q_5mod8.
+      assert (0 <= q/8)%Z by (apply Z.div_le_lower_bound; rewrite ?Z.mul_0_r; omega).
+      assert (Z.to_N (q / 8 + 1) <> 0%N) by
+          (intro Hbad; change (0%N) with (Z.to_N 0%Z) in Hbad; rewrite Z2N.inj_iff in Hbad; omega).
+      destruct (dec (x = 0)); [subst; rewrite !pow_0_l by (trivial || lazy_decide); reflexivity|].
+      rewrite !pow_pow_l.
+
+      replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N.
+      Focus 2. { (* this is a boring but gnarly proof :/ *)
+        change (2*2)%N with (Z.to_N 4).
+        rewrite <- Z2N.inj_mul by zero_bounds.
+        apply Z2N.inj_iff; try zero_bounds.
+        rewrite <- Z.mul_cancel_l with (p := 2) by omega.
+        ring_simplify.
+        rewrite Z.mul_div_eq by omega.
+        rewrite Z.mul_div_eq by omega.
+        rewrite (Zmod_div_mod 2 8 q) by
+            (try omega; apply Zmod_divide; omega || auto).
+        rewrite q_5mod8.
+        replace (5 mod 2)%Z with 1%Z by auto.
+        ring.
+      } Unfocus.
+
+      rewrite Z2N.inj_add, pow_add_r by zero_bounds.
+      replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1) by
+          (symmetry; apply @euler_criterion; eauto).
+      change (Z.to_N 2) with 2%N; ring.
+    Qed.
 
-      Focus 2.
-      replace 4%N with (Z.to_N 4) by auto.
-      rewrite <- Z2N.inj_mul by zero_bounds.
-      apply Z2N.inj_iff; try zero_bounds.
-      rewrite <- Z.mul_cancel_l with (p := 2) by omega.
+    Lemma sqrt_5mod8_valid : forall x, (exists y, y*y = x) ->
+                                       (sqrt_5mod8 x)*(sqrt_5mod8 x) = x.
+    Proof.
+      intros x x_square.
+      pose proof (eq_b4_a2 x x_square) as Hyy; rewrite !pow_2_r in Hyy.
+      destruct (Algebra.only_two_square_roots_choice _ x (x*x) Hyy eq_refl) as [Hb|Hb]; clear Hyy;
+        unfold sqrt_5mod8; break_if; rewrite !@pow_2_r in *; intuition.
       ring_simplify.
-      rewrite Z.mul_div_eq by omega.
-      rewrite Z.mul_div_eq by omega.
-      rewrite (Zmod_div_mod 2 8 q) by
-        (try omega; apply Zmod_divide; omega || auto).
-      rewrite q_5mod8.
-      replace (5 mod 2)%Z with 1%Z by auto.
-      ring.
-      (* End Focus *)
-
-      rewrite Z2N.inj_add by zero_bounds.
-      rewrite <- F_pow_add by zero_bounds.
-      replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1).
-      replace (Z.to_N 2) with 2%N by auto.
-      ring.
-
-      symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8.
-    }
-  Qed.
-
-  Lemma sqrt_mod_q_valid : forall x, isSquare x ->
-    (sqrt_mod_q x) ^ 2 = x.
-  Proof.
-    intros x x_square.
-    destruct (sqrt_solutions x _ (eq_b4_a2 x x_square)) as [? | eq_b2_oppx];
-      unfold sqrt_mod_q; break_if; intuition.
-    ring_simplify.
-    unfold sqrt_minus1.
-    rewrite sqrt_minus1_valid.
-    rewrite eq_b2_oppx.
-    field.
-  Qed.
-
-  Lemma sqrt_mod_q_of_0 : sqrt_mod_q 0 = 0.
-  Proof.
-    unfold sqrt_mod_q.
-    rewrite !Fq_pow_zero.
-    break_if; ring.
-
-    congruence.
-    intro false_eq.
-    rewrite <-(N2Z.id 0) in false_eq.
-    rewrite N2Z.inj_0 in false_eq.
-    pose proof (prime_ge_2 q prime_q).
-    apply Z2N.inj in false_eq; zero_bounds.
-    assert (0 < q / 8 + 1)%Z.
-    apply Z.add_nonneg_pos; zero_bounds.
-    omega.
-  Qed.
-
-  Lemma sqrt_mod_q_root_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0.
-  Proof.
-    unfold sqrt_mod_q; intros.
-    break_if.
-    - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end.
+      unfold sqrt_minus1; rewrite @pow_2_r.
+      rewrite sqrt_minus1_valid; rewrite @pow_2_r.
+      rewrite Hb.
       ring.
-    - match goal with
-      | [H : sqrt_minus1 * _ = 0 |- _ ]=>
-         apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ];
-         [ | eapply Fq_root_zero; eauto ]
-      end.
-      unfold sqrt_minus1 in sqrt_minus1_zero.
-      rewrite sqrt_minus1_zero in sqrt_minus1_valid.
-      exfalso.
-      pose proof (@F_opp_spec q 1) as opp_spec_1.
-      rewrite <-sqrt_minus1_valid in opp_spec_1.
-      assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring.
-      rewrite ring_subst in *.
-      apply Fq_1_neq_0; assumption.
-  Qed.
-
-End SquareRootsPrime5Mod8.
-
-Local Open Scope F_scope.
-(** Tactics for solving inequalities. *)
-Ltac solve_cancel_by_field y tnz :=
-  solve [ generalize dependent y; intros;
-          field; tnz ].
-
-Ltac cancel_nonzero_factors' tnz :=
-  idtac;
-  match goal with
-  | [ |- ?x = 0 -> False ]
-    => change (x <> 0)
-  | [ |- ?x * ?y <> 0 ]
-    => apply Fq_mul_nonzero_nonzero
-  | [ H : ?y <> 0 |- _ ]
-    => progress rewrite ?(add_cancel_mul_r_nonzero H), ?(sub_cancel_mul_r_nonzero H), ?(add_cancel_l_nonzero H), ?(sub_cancel_l_nonzero H);
-       apply Fq_mul_nonzero_nonzero; [ | assumption ]
-  | [ |- ?op (?y * (ZToField (m := ?q) ?n)) ?z <> 0 ]
-    => unique assert (ZToField (m := q) n <> 0) by tnz;
-       generalize dependent (ZToField (m := q) n); intros
-  | [ |- ?op (?x * (?y * ?z)) _ <> 0 ]
-    => rewrite F_mul_assoc
-  end.
-Ltac cancel_nonzero_factors tnz := repeat cancel_nonzero_factors' tnz.
-Ltac specialize_quantified_equalities :=
-  repeat match goal with
-         | [ H : forall _ _ _ _, _ = _ -> _, H' : _ = _ |- _ ]
-           => unique pose proof (fun x2 y2 => H _ _ x2 y2 H')
-         | [ H : forall _ _, _ = _ -> _, H' : _ = _ |- _ ]
-           => unique pose proof (H _ _ H')
-         end.
-Ltac finish_inequality tnz :=
-  idtac;
-  match goal with
-  | [ H : ?x <> 0 |- ?y <> 0 ]
-    => replace y with x by (field; tnz); exact H
-  end.
-Ltac field_nonzero tnz :=
-  cancel_nonzero_factors tnz;
-  try (specialize_quantified_equalities;
-       progress cancel_nonzero_factors tnz);
-  try solve [ specialize_quantified_equalities;
-              finish_inequality tnz ].
+    Qed.
+  End SquareRootsPrime5Mod8.
+End Zmod.
\ No newline at end of file
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index 7d354ab3e..999c61971 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -11,17 +11,16 @@ Section Mod24.
   Let q := 24.
 
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
+  Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [ring]. Similar boilerplate works for [field] if
   the modulus is prime . *)
-  Add Ring Fring_q : (@Fring_theory q)
-    (morphism (@Fring_morph q),
-     preprocess [unfold ZToFq; Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
+  Add Ring _theory : (Zmod.ring_theory q)
+    (morphism (Zmod.ring_morph q),
+     preprocess [unfold ZToFq],
+     constants [Zmod.is_constant],
+     div (Zmod.morph_div_theory q),
+     power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]).
 
   Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
   Proof.
@@ -39,34 +38,33 @@ Section Modq.
   Local Open Scope F_scope.
 
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
+  Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [field]. Similar boilerplate works for [ring] if
   the modulus is not prime . *)
-  Add Field Ffield_q' : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [unfold ZToFq; Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
-
-  Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
+  Add Field _theory' : (Zmod.field_theory q)
+    (morphism (Zmod.ring_morph q),
+     preprocess [unfold ZToFq],
+     constants [Zmod.is_constant],
+     div (Zmod.morph_div_theory q),
+     power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]).
+
+  Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + 2*(a/c)*(b/c) + b^2/c^2.
   Proof.
     intros.
-    field.
+    field; trivial.
   Qed.
 End Modq.
 
 (*** The old way: Modules ***)
 
-Module Modulus31 <: PrimeModulus.
+Module Modulus31 <: Zmod.PrimeModulus.
   Definition modulus := 2^5 - 1.
   Lemma prime_modulus : prime modulus.
   Admitted.
 End Modulus31.
 
-Module Modulus127 <: PrimeModulus.
+Module Modulus127 <: Zmod.PrimeModulus.
   Definition modulus := 2^127 - 1.
   Lemma prime_modulus : prime modulus.
   Admitted.
@@ -74,14 +72,14 @@ End Modulus127.
 
 Module Example31.
   (* Then we can construct a field with that modulus *)
-  Module Import Field := FieldModulo Modulus31.
+  Module Import Field := Zmod.FieldModulo Modulus31.
   Import Modulus31.
 
   (* And pull in the appropriate notations *)
   Local Open Scope F_scope.
 
   (* First, let's solve a ring example*)
-  Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x.
+  Lemma ring_example: forall x: F modulus, x * (ZToField _ 2) = x + x.
   Proof.
     intros.
     ring.
@@ -92,7 +90,7 @@ Module Example31.
     Therefore, it is necessary to explicitly rewrite the modulus
     (usually hidden by implicitn arguments) match the one passed to
     [FieldModulo]. *)
-  Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x.
+  Lemma ring_example': forall x: F (2^5-1), x * (ZToField _ 2) = x + x.
   Proof.
     intros.
     change (2^5-1)%Z with modulus.
@@ -108,7 +106,7 @@ Module Example31.
   Qed.
 
   (* Then an example with exponentiation *)
-  Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2.
+  Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField _ 2 * x + 1 = (x + 1) ^ 2.
   Proof.
     intros; simpl.
     field; trivial.
@@ -143,7 +141,7 @@ End Example31.
 
 (* Notice that the field tactics work whether we know what the modulus is *)
 Module TimesZeroTransparentTestModule.
-  Module Import Theory := FieldModulo Modulus127.
+  Module Import Theory := Zmod.FieldModulo Modulus127.
   Import Modulus127.
   Local Open Scope F_scope.
 
@@ -153,9 +151,13 @@ Module TimesZeroTransparentTestModule.
   Qed.
 End TimesZeroTransparentTestModule.
 
-(* Or if we don't (i.e. it's opaque) *)
-Module TimesZeroParametricTestModule (M: PrimeModulus).
-  Module Theory := FieldModulo M.
+(* An opaque modulus causes the field tactic to expand all constants
+  into matches on the modulus. Goals can still be proven, but with
+  significant overhead. Consider using an entirely abstract
+  [Algebra.field] instead. *)
+  
+Module TimesZeroParametricTestModule (M: Zmod.PrimeModulus).
+  Module Theory := Zmod.FieldModulo M.
   Import Theory M.
   Local Open Scope F_scope.
 
@@ -164,26 +166,27 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field.
   Qed.
 
-  Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
+  Lemma realisticFraction : forall x y d : F modulus, 1 <> ZToField modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
   Proof.
     intros.
-    field; try exact Fq_1_neq_0.
+    field; assumption.
   Qed.
 
   Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
+   1 <> ZToField modulus 0 -> 
    ZQ <> 0 ->
    ZP <> 0 ->
    ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
-   ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
-   ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+   ZP * ZToField _ 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 ->
+   ZP * ZToField _ 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 ->
 
    ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
-   (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
-   ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-    (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) =
+   (ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) /
+   ((ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) *
+    (ZP * ZToField _ 2 * ZQ + XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ))) =
    (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)).
   Proof.
     intros.
-    field; assumption.
+    field; repeat split; assumption.
   Qed.
 End TimesZeroParametricTestModule.