diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-25 00:03:49 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-25 00:03:49 -0400 |
| commit | a5e707be4ea86ecf0ad40fc0f0b1c1029a9b88b0 (patch) | |
| tree | 154c23023c2285245ee3b9ad6fdc2115d53fba0d /src/CompleteEdwardsCurve | |
| parent | 7325795b833b58175eac79b6fd224d409a82f941 (diff) | |
update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index f85e2870c..ed4511fc9 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -32,6 +32,7 @@ Section Pre. Lemma onCurve_subst : forall x1 x2 y1 y2, and (eq x1 y1) (eq x2 y2) -> onCurve (x1, x2) -> onCurve (y1, y2). Proof. + unfold onCurve. intros ? ? ? ? [eq_1 eq_2] ?. rewrite eq_1, eq_2 in *. assumption. |