diff options
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index be423c05c..ed4511fc9 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -29,6 +29,15 @@ Section Pre. Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. + 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. + Qed. + Lemma edwardsAddComplete' x1 y1 x2 y2 : onCurve (pair x1 y1) -> onCurve (pair x2 y2) -> |