From a5e707be4ea86ecf0ad40fc0f0b1c1029a9b88b0 Mon Sep 17 00:00:00 2001 From: jadep Date: Sat, 25 Jun 2016 00:03:49 -0400 Subject: update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file --- src/CompleteEdwardsCurve/Pre.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/CompleteEdwardsCurve') 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. -- cgit v1.2.3