From 60d4c8b55dd7cbede0ebb69ac3678b8f451342ef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 10:53:17 -0400 Subject: Simplify proof of proj1_fe25519_encode --- src/Specific/GF25519BoundedCommon.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'src/Specific') 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. -- cgit v1.2.3