diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 14:44:48 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-12 14:45:10 -0500 |
| commit | 34875f01c422e5665a73f076e7e17b9c7e1d5aa0 (patch) | |
| tree | 378f93450b3515858b12b6404e52031a92eae50d /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 41b48a78924a9689b9ab838eb74b1d14f267cdfe (diff) | |
port some edwards curve theorems
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 338903b26..6a862fb3b 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -56,7 +56,7 @@ Section VariousModPrime. Add Field Ffield_Z : (@Ffield_theory q _) (morphism (@Fring_morph q), preprocess [Fpreprocess], - postprocess [Fpostprocess], + postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], constants [Fconstant], div (@Fmorph_div_theory q), power_tac (@Fpower_theory q) [Fexp_tac]). @@ -133,6 +133,11 @@ Section VariousModPrime. + intuition. + apply IHp; auto. 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 sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. |