diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-11 17:57:57 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-11 17:57:57 -0500 |
| commit | 7ce9586da796da9e7656e691f8e63d4f59257649 (patch) | |
| tree | 48540d4c39ba8ccbbda1572f97181038cdeada08 /src/Specific | |
| parent | 056018a4ade16f17fca77289d8f6443f31b59496 (diff) | |
port several theorems from GF to F
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/EdDSA25519.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 96f997180..6403c8b53 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -557,7 +557,8 @@ Module EdDSA25519_Params <: EdDSAParams. I have so far not managed to unify them. *) Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 -> forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. - Admitted. + apply Facts.point_eq. + Qed. Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. Proof. |