diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-24 23:47:43 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-24 23:47:43 -0400 |
| commit | 7325795b833b58175eac79b6fd224d409a82f941 (patch) | |
| tree | 7d44b0664bd8e866a30a251c08e6e77586bca6a5 /src/CompleteEdwardsCurve/Pre.v | |
| parent | 377c567946c7d12eabafc0cf4b91ed0bf1d1d997 (diff) | |
| parent | 65dad95295378962770304dbf4368975fe46c7dc (diff) | |
Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_port
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 133a21605..f85e2870c 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -49,7 +49,7 @@ Section Pre. => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) /(f (sqrt_a * x2) y2 * x1 * y1 )) | _ => apply a_nonzero - end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict. + end; field_algebra; auto using Ring.opp_nonzero_nonzero; nsatz_contradict. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : |