From 7f5ded6a82327e5dc97ecd4ff300379ddd93dba5 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sun, 29 May 2016 17:45:53 -0400
Subject: ERep add

---
 src/CompleteEdwardsCurve/ExtendedCoordinates.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/CompleteEdwardsCurve')

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 96365084c..44033097d 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -181,6 +181,14 @@ Section ExtendedCoordinates.
         unfold rep in *; intuition.
     Qed.
 
+    Lemma unifiedAddM1_correct : forall P Q, mkExtendedPoint (E.add P Q) === unifiedAddM1 (mkExtendedPoint P) (mkExtendedPoint Q).
+    Proof.
+      unfold equiv, extendedPoint_eq; intros;
+        pose proof unifiedAddM1_rep (mkExtendedPoint P) (mkExtendedPoint Q);
+        pose proof unExtendedPoint_mkExtendedPoint;
+        congruence.
+    Qed.
+
     Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1.
     Proof.
       repeat (econstructor || intro).
-- 
cgit v1.2.3