remove duplicate axiom

1 files changed, 1 insertions, 4 deletions

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).