diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:26:13 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:26:13 -0400 |
| commit | 65c3c384aec8216d4d7f9a6fc50d83201035daf5 (patch) | |
| tree | ede582062c0e193858c7f986941774900841f8f7 /src/CompleteEdwardsCurve | |
| parent | 6fd9bd39da9cb1e85c5b1fe14bac282a1a038cb1 (diff) | |
Integrate Pseudize into Pipeline.v
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index c1b0e7d71..be8ca24a2 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -60,17 +60,6 @@ Section Pre. unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. Qed. - - Lemma jason : forall (x y: F), - x^2 = y^2 -> x <> 0-y -> x <> y -> False. - Proof. - intros x y A B C; destruct (eq_dec (x - y) 0). - - - contradict C. field_algebra. - - assert ((x + y) = 0 / (x - y)) as Z by (field_simplify_eq_all; field_algebra). - replace (0 / _) with 0 in Z by admit. - contradict B; field_algebra. - Admitted. End Pre. Import Group Ring Field. |