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/Tutorial.v | |
| parent | 41b48a78924a9689b9ab838eb74b1d14f267cdfe (diff) | |
port some edwards curve theorems
Diffstat (limited to 'src/ModularArithmetic/Tutorial.v')
| -rw-r--r-- | src/ModularArithmetic/Tutorial.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index e84659c9e..a4cbcb5ca 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -104,5 +104,12 @@ Module TimesZeroParametricTestModule (M: PrimeModulus). intros. field. Qed. + + Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. + Proof. + intros. + field; try exact Fq_1_neq_0. + Qed. + End TimesZeroParametricTestModule. |