Pseudize Let_In

1 files changed, 14 insertions, 1 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index be294fb3e..c1b0e7d71 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -4,7 +4,9 @@ Require Import Crypto.Util.Notations.
 
 Generalizable All Variables.
 Section Pre.
-  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Context {F eq zero one opp add sub mul inv div}
+         `{field F eq zero one opp add sub mul inv div}.
+
   Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
   Local Notation "0" := zero.  Local Notation "1" := one.
@@ -58,6 +60,17 @@ 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.