diff options
Diffstat (limited to 'src/Curves/Edwards/Pre.v')
| -rw-r--r-- | src/Curves/Edwards/Pre.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v index 244acc9b5..9f5d5cfab 100644 --- a/src/Curves/Edwards/Pre.v +++ b/src/Curves/Edwards/Pre.v @@ -43,4 +43,4 @@ Section Edwards. Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed. End Addition. -End Edwards.
\ No newline at end of file +End Edwards. |