diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 10:53:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 10:53:17 -0400 |
| commit | 60d4c8b55dd7cbede0ebb69ac3678b8f451342ef (patch) | |
| tree | 24a2782e96b48405f2fd2561afef2dd75a1fa401 /src/Specific | |
| parent | f0f90dbc7bc056266a520a390dbff662e260c08b (diff) | |
Simplify proof of proj1_fe25519_encode
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index aea3ff4c2..511370c63 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -387,9 +387,7 @@ Definition decode (x : fe25519) : F modulus Lemma proj1_fe25519_encode x : proj1_fe25519 (encode x) = ModularBaseSystem.encode x. -Proof. - hnf in x; destruct_head' prod; reflexivity. -Qed. +Proof. reflexivity. Qed. Lemma decode_exist_fe25519 x pf : decode (exist_fe25519 x pf) = ModularBaseSystem.decode x. |