prove ring admits

1 files changed, 1 insertions, 3 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fdb859560..c0b1b56d6 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -23,8 +23,6 @@ Section Pre.
     let (x1, y1) := P1' in
     let (x2, y2) := P2' in
     pair (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-
-  Lemma opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0. Admitted.
   
   Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
 
@@ -40,7 +38,7 @@ Section Pre.
         => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
                                            /(f (sqrt_a * x2) y2   *   x1 * y1           ))
       | _ => apply a_nonzero
-      end; field_algebra; auto using opp_nonzero_nonzero.
+      end; field_algebra; auto using Ring.opp_nonzero_nonzero.
   Qed.
 
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :