From 96cec1597d70511e922a8c032845a09f0205b1a9 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 16 Jan 2016 16:53:46 -0500 Subject: remove duplicate axiom --- src/Curves/PointFormats.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'src') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 49c3b9ba3..a44ed7a6d 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -412,6 +412,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam | N.pos p => iter_op unifiedAdd zero b p b P end. + Hint Resolve char_gt_2. End CompleteTwistedEdwardsCurve. @@ -702,10 +703,6 @@ Module ExtendedM1 (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEd Delimit Scope extendedM1_scope with extendedM1. Infix "+" := unifiedAdd : extendedM1_scope. - Lemma char_gt_2 : 2 <> 0. - Admitted. - Hint Resolve char_gt_2. - Local Hint Unfold unifiedAdd'. Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). -- cgit v1.2.3