use [positive] for [F] modulus, char_ge_C instead of char_gt_C

7 files changed, 48 insertions, 281 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 262b20e3e..863300dde 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -31,8 +31,15 @@ Module F.
   Lemma pow_spec {m} a : F.pow a 0%N = 1%F :> F m /\ forall x, F.pow a (1 + x)%N = F.mul a (F.pow a x).
   Proof. change (@F.pow m) with (proj1_sig (@F.pow_with_spec m)); destruct (@F.pow_with_spec m); eauto. Qed.
 
+  Global Instance char_gt {m} :
+    @Ring.char_ge
+      (F m) Logic.eq F.zero F.one F.opp F.add F.sub F.mul
+      m.
+  Proof.
+  Admitted.
+
   Section FandZ.
-    Context {m:Z}.
+    Context {m:positive}.
     Local Open Scope F_scope.
 
     Theorem eq_to_Z_iff (x y : F m) : x = y <-> F.to_Z x = F.to_Z y.
@@ -145,34 +152,33 @@ Module F.
     Local Infix "mod" := modulo : nat_scope.
     Local Open Scope nat_scope.
 
-    Context {m} (m_pos: (0 < m)%Z).
-    Let to_nat_m_nonzero : Z.to_nat m <> 0.
-      rewrite Z2Nat.inj_lt in m_pos; omega.
-    Qed.
+    Context {m:BinPos.positive}.
 
     Lemma to_nat_of_nat (n:nat) : F.to_nat (F.of_nat m n) = (n mod (Z.to_nat m))%nat.
     Proof.
       unfold F.to_nat, F.of_nat.
       rewrite F.to_Z_of_Z.
-      pose proof (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero) as Hmod.
-      rewrite Z2Nat.id in Hmod by omega.
+      assert (Pos.to_nat m <> 0)%nat as HA by (pose proof Pos2Nat.is_pos m; omega).
+      pose proof (mod_Zmod n (Pos.to_nat m) HA) as Hmod.
+      rewrite positive_nat_Z in Hmod.
       rewrite <- Hmod.
-      rewrite <-Nat2Z.id by omega.
-      reflexivity.
+      rewrite <-Nat2Z.id, Z2Nat.inj_pos; omega.
     Qed.
 
     Lemma of_nat_to_nat x : F.of_nat m (F.to_nat x) = x.
       unfold F.to_nat, F.of_nat.
-      rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; trivial].
+      rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; reflexivity].
     Qed.
 
+    Lemma Pos_to_nat_nonzero p : Pos.to_nat p <> 0%nat.
+    Admitted.
+
     Lemma of_nat_mod (n:nat) : F.of_nat m (n mod (Z.to_nat m)) = F.of_nat m n.
     Proof.
       unfold F.of_nat.
-      replace (Z.of_nat (n mod Z.to_nat m)) with(Z.of_nat n mod Z.of_nat (Z.to_nat m))%Z
-        by (symmetry; eapply (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero)).
-      rewrite Z2Nat.id by omega.
-      rewrite <-F.of_Z_mod; reflexivity.
+      rewrite (F.of_Z_mod (Z.of_nat n)), ?mod_Zmod, ?Z2Nat.id; [reflexivity|..].
+      { apply Pos2Z.is_nonneg. }
+      { rewrite Z2Nat.inj_pos. apply Pos_to_nat_nonzero. }
     Qed.
 
     Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x.
@@ -192,7 +198,7 @@ Module F.
   End FandNat.
 
   Section RingTacticGadgets.
-    Context (m:Z).
+    Context (m:positive).
 
     Definition ring_theory : ring_theory 0%F 1%F (@F.add m) (@F.mul m) (@F.sub m) (@F.opp m) eq
       := Algebra.Ring.ring_theory_for_stdlib_tactic.
@@ -252,22 +258,8 @@ Module F.
   Ltac is_constant t := match t with F.of_Z _ ?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}.
+    Context {m:positive}.
     Local Open Scope F_scope.
 
     Add Ring _theory : (ring_theory m)
@@ -284,7 +276,7 @@ Module F.
   End VariousModulo.
 
   Section Pow.
-    Context {m:Z}.
+    Context {m:positive}.
     Add Ring _theory' : (ring_theory m)
                           (morphism (ring_morph m),
                            constants [is_constant],
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index fd9483182..428239498 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -164,7 +164,7 @@ Section ModulusDigitsProofs.
     rewrite encodeZ_spec by eauto using limb_widths_nonnil, limb_widths_good.
     apply Z.mod_small.
     cbv [upper_bound]. fold k.
-    assert (modulus = 2 ^ k - c) by (cbv [c]; ring).
+    assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring).
     omega.
   Qed.
 
@@ -182,7 +182,7 @@ Section ModulusDigitsProofs.
            | |- _ => progress autorewrite with Ztestbit
            | |- _ => unique pose proof c_pos
            | |- _ => unique pose proof modulus_pos
-           | |- _ => unique assert (modulus = 2 ^ k - c) by (cbv [c]; ring)
+           | |- _ => unique assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring)
            | |- _ => break_if
            | |- _ => rewrite decode_modulus_digits
            | |- _ => rewrite Z.testbit_pow2_mod
@@ -196,7 +196,7 @@ Section ModulusDigitsProofs.
                specialize_by (eauto || omega);
                rewrite sum_firstn_succ_default in *; split; zero_bounds; eauto)
            | |- Z.pow2_mod _ _ = Z.ones _ => apply Z.bits_inj'
-           | |- Z.testbit modulus ?i = true => transitivity (Z.testbit (2 ^ k - c) i)
+           | |- Z.testbit (Z.pos modulus) ?i = true => transitivity (Z.testbit (2 ^ k - c) i)
            | |- _ => congruence
            end.
 
@@ -496,7 +496,7 @@ Section ConditionalSubtractModulusProofs.
     specialize_by auto.
     cbv [upper_bound] in *.
     fold k in *.
-    assert (modulus = 2 ^ k - c) by (cbv [c]; ring).
+    assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring).
     destruct (Z_le_dec modulus (BaseSystem.decode base u)).
     + split; try omega.
       apply Z.lt_le_trans with (m := 2 ^ k); try omega.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 3b0231191..34a331fa1 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -30,12 +30,12 @@ Class CarryChain (limb_widths : list Z) :=
     carry_chain_valid : forall i, In i carry_chain -> (i < length limb_widths)%nat
   }.
 
-  Class SubtractionCoefficient {m : Z} {prm : PseudoMersenneBaseParams m} := {
+  Class SubtractionCoefficient {m : positive} {prm : PseudoMersenneBaseParams m} := {
     coeff : tuple Z (length limb_widths);
     coeff_mod: decode coeff = 0%F
   }.
 
-  Class ExponentiationChain {m : Z} {prm : PseudoMersenneBaseParams m} (exp : Z) := {
+  Class ExponentiationChain {m : positive} {prm : PseudoMersenneBaseParams m} (exp : Z) := {
     chain : list (nat * nat);
     chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N exp
   }.
@@ -85,7 +85,7 @@ Section FieldOperationProofs.
     + apply F.of_Z_to_Z.
     + apply bv.
     + rewrite <-F.mod_to_Z.
-      match goal with |- appcontext [?a mod modulus] =>
+      match goal with |- appcontext [?a mod (Z.pos modulus)] =>
                       pose proof (Z.mod_pos_bound a modulus modulus_pos) end.
       pose proof lt_modulus_2k.
       omega.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index abc30056f..6f2970814 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -15,10 +15,11 @@ Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.Algebra Crypto.Algebra.Field.
 
 Existing Class prime.
+Local Open Scope F_scope.
 
 Module F.
   Section Field.
-    Context (q:Z) {prime_q:prime q}.
+    Context (q:positive) {prime_q:prime q}.
     Lemma inv_spec : F.inv 0%F = (0%F : F q)
                      /\ (prime q -> forall x : F q, x <> 0%F -> (F.inv x * x)%F = 1%F).
     Proof. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed.
@@ -37,33 +38,10 @@ Module F.
              | _ => split
              end.
     Qed.
-
-    Definition field_theory : field_theory 0%F 1%F F.add F.mul F.sub F.opp F.div F.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 := F.RingModulo M.
-    Add Field _field : (F.field_theory modulus)
-                         (morphism (F.ring_morph modulus),
-                          constants [F.is_constant],
-                          div (F.morph_div_theory modulus),
-                          power_tac (F.power_theory modulus) [F.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 (F.ring_morph q),
-                          constants [F.is_constant],
-                          div (F.morph_div_theory q),
-                          power_tac (F.power_theory q) [F.is_pow_constant]).
+    Context {q:positive} {prime_q:prime q} {two_lt_q: 2 < q}.
 
     (* TODO: move to PrimeFieldTheorems *)
     Lemma to_Z_1 : @F.to_Z q 1 = 1%Z.
@@ -91,16 +69,15 @@ Module F.
     Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x).
     Proof.
       destruct (dec (x = 0)).
-      { left. abstract (exists 0; subst; ring). }
+      { left. abstract (exists 0; subst; apply Ring.mul_0_l). }
       { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. }
     Defined.
   End NumberThoery.
 
   Section SquareRootsPrime3Mod4.
-    Context {q:Z} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}.
+    Context {q:positive} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}.
 
-    Local Open Scope F_scope.
-    Add Field _field2 : (field_theory q)
+    Add Field _field2 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q))
                           (morphism (F.ring_morph q),
                            constants [F.is_constant],
                            div (F.morph_div_theory q),
@@ -114,15 +91,13 @@ Module F.
     Lemma two_lt_q_3mod4 : 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.
+      destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|].
+      rewrite <-H in q_3mod4; discriminate.
     Qed.
     Local Hint Resolve two_lt_q_3mod4.
     
-    Lemma sqrt_3mod4_correct : forall x,
-      ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x).
+    Lemma sqrt_3mod4_correct (x:F q) :
+      ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F.
     Proof.
       cbv [sqrt_3mod4]; intros.
       destruct (F.eq_dec x 0);
@@ -148,10 +123,9 @@ Module F.
   End SquareRootsPrime3Mod4.
 
   Section SquareRootsPrime5Mod8.
-    Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
-
+    Context {q:positive} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
     Local Open Scope F_scope.
-    Add Field _field3 : (field_theory q)
+    Add Field _field3 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q))
                           (morphism (F.ring_morph q),
                            constants [F.is_constant],
                            div (F.morph_div_theory q),
@@ -164,10 +138,8 @@ Module F.
     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.
+      destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|].
+      rewrite <-H in *. discriminate.
     Qed.
     Local Hint Resolve two_lt_q_5mod8.
 
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 630fc102e..3a530c377 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -33,7 +33,7 @@ Section PseudoMersenneBaseParamProofs.
     pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega.
   Qed. Hint Resolve modulus_pos.
 
-  Lemma modulus_nonzero : modulus <> 0.
+  Lemma modulus_nonzero : Z.pos modulus <> 0.
     pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega.
   Qed.
 
@@ -45,7 +45,6 @@ Section PseudoMersenneBaseParamProofs.
     rewrite Z.mul_add_distr_r, Zplus_mod.
     unfold c.
     rewrite Z.sub_sub_distr, Z.sub_diag.
-    simpl.
     rewrite Z.mul_comm, Z.mod_add_l; auto using modulus_nonzero.
     rewrite <- Zplus_mod; auto.
   Qed.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v
index b564bcb05..6f6fd6556 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParams.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v
@@ -4,16 +4,16 @@ Require Import Crypto.Util.ListUtil.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
-Class PseudoMersenneBaseParams (modulus : Z) := {
+Class PseudoMersenneBaseParams (modulus : positive) := {
   limb_widths : list Z;
   limb_widths_pos : forall w, In w limb_widths -> 0 < w;
   limb_widths_nonnil : limb_widths <> nil;
   limb_widths_good : forall i j, (i + j < length limb_widths)%nat ->
     sum_firstn limb_widths (i + j) <=
     sum_firstn limb_widths i + sum_firstn limb_widths j;
-  prime_modulus : Znumtheory.prime modulus;
+  prime_modulus : Znumtheory.prime (Z.pos modulus);
   k := sum_firstn limb_widths (length limb_widths);
-  c := 2 ^ k - modulus;
+  c := 2 ^ k - (Z.pos modulus);
   c_pos : 0 < c;
   limb_widths_match_modulus : forall i j,
     (i < length limb_widths)%nat ->
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
deleted file mode 100644
index 4ec1ed82c..000000000
--- a/src/ModularArithmetic/Tutorial.v
+++ /dev/null
@@ -1,196 +0,0 @@
-Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
-
-
-(* Example for modular arithmetic with a concrete modulus in a section *)
-Section Mod24.
-  (* Set notations + - * / refer to F operations *)
-  Local Open Scope F_scope.
-
-  (* Specify modulus *)
-  Let q := 24.
-
-  (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq.
-  Local Coercion ZToFq : Z >-> F.
-  Local Coercion F.to_Z : F >-> Z.
-
-  (* Boilerplate for [ring]. Similar boilerplate works for [field] if
-  the modulus is prime . *)
-  Add Ring _theory : (F.ring_theory q)
-    (morphism (F.ring_morph q),
-     preprocess [unfold ZToFq],
-     constants [F.is_constant],
-     div (F.morph_div_theory q),
-     power_tac (F.power_theory q) [F.is_pow_constant]).
-
-  Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
-  Proof.
-    intros.
-    ring.
-  Qed.
-End Mod24.
-
-(* Example for modular arithmetic with an abstract modulus in a section *)
-Section Modq.
-  Context {q:Z} {prime_q:prime q}.
-  Existing Instance prime_q.
-
-  (* Set notations + - * / refer to F operations *)
-  Local Open Scope F_scope.
-
-  (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq.
-  Local Coercion ZToFq : Z >-> F.
-  Local Coercion F.to_Z : F >-> Z.
-
-  (* Boilerplate for [field]. Similar boilerplate works for [ring] if
-  the modulus is not prime . *)
-  Add Field _theory' : (F.field_theory q)
-    (morphism (F.ring_morph q),
-     preprocess [unfold ZToFq],
-     constants [F.is_constant],
-     div (F.morph_div_theory q),
-     power_tac (F.power_theory q) [F.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; trivial.
-  Qed.
-End Modq.
-
-(*** The old way: Modules ***)
-
-Module Modulus31 <: F.PrimeModulus.
-  Definition modulus := 2^5 - 1.
-  Lemma prime_modulus : prime modulus.
-  Admitted.
-End Modulus31.
-
-Module Modulus127 <: F.PrimeModulus.
-  Definition modulus := 2^127 - 1.
-  Lemma prime_modulus : prime modulus.
-  Admitted.
-End Modulus127.
-
-Module Example31.
-  (* Then we can construct a field with that modulus *)
-  Module Import Field := F.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 * (F.of_Z _ 2) = x + x.
-  Proof.
-    intros.
-    ring.
-  Qed.
-
-  (* Unfortunately, the [ring] and [field] tactics need syntactic
-    (not definitional) equality to recognize the ring in question.
-    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 * (F.of_Z _ 2) = x + x.
-  Proof.
-    intros.
-    change (2^5-1)%Z with modulus.
-    ring.
-  Qed.
-
-  (* Then a field example (we have to know we can't divide by zero!) *)
-  Lemma field_example: forall x y z: F modulus, z <> 0 ->
-    x * (y / z) / z = x * y / (z ^ 2).
-  Proof.
-    intros; simpl.
-    field; trivial.
-  Qed.
-
-  (* Then an example with exponentiation *)
-  Lemma exp_example: forall x: F modulus, x ^ 2 + F.of_Z _ 2 * x + 1 = (x + 1) ^ 2.
-  Proof.
-    intros; simpl.
-    field; trivial.
-  Qed.
-
-  (* In general, the rule I've been using is:
-
-     - If our goal looks like x = y:
-
-        + If we need to use assumptions to prove the goal, then before
-          we apply field,
-
-          * Perform all relevant substitutions (especially subst)
-
-          * If we have something more complex, we're probably going
-            to have to performe some sequence of "replace X with Y"
-            and solve out the subgoals manually before we can use
-            field.
-
-        + Else, just use field directly
-
-     - If we just want to simplify terms and put them into a canonical
-       form, then field_simplify or ring_simplify should do the trick.
-       Note, however, that the canonical form has lots of annoying "/1"s
-
-     - Otherwise, do a "replace X with Y" to generate an equality
-       so that we can use field in the above case
-
-     *)
-
-End Example31.
-
-(* Notice that the field tactics work whether we know what the modulus is *)
-Module TimesZeroTransparentTestModule.
-  Module Import Theory := F.FieldModulo Modulus127.
-  Import Modulus127.
-  Local Open Scope F_scope.
-
-  Lemma timesZero : forall a : F modulus, a*0 = 0.
-    intros.
-    field.
-  Qed.
-End TimesZeroTransparentTestModule.
-
-(* 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: F.PrimeModulus).
-  Module Theory := F.FieldModulo M.
-  Import Theory M.
-  Local Open Scope F_scope.
-
-  Lemma timesZero : forall a : F modulus, a*0 = 0.
-    intros.
-    field.
-  Qed.
-
-  Lemma realisticFraction : forall x y d : F modulus, 1 <> F.of_Z modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
-  Proof.
-    intros.
-    field; assumption.
-  Qed.
-
-  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
-   1 <> F.of_Z modulus 0 -> 
-   ZQ <> 0 ->
-   ZP <> 0 ->
-   ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
-   ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) + XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 ->
-   ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) - XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 ->
-
-   ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
-   (ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) /
-   ((ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) *
-    (ZP * F.of_Z _ 2 * ZQ + XP * YP / ZP * F.of_Z _ 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; repeat split; assumption.
-  Qed.
-End TimesZeroParametricTestModule.