remove field_algebra

1 files changed, 6 insertions, 10 deletions

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 263582508..d8efb82f3 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -33,6 +33,7 @@ Module Extended.
     Create HintDb bash discriminated.
     Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash.
     Ltac bash :=
+      pose proof E.char_gt_2;
       repeat match goal with
              | |- Proper _ _ => intro
              | _ => progress intros
@@ -43,15 +44,11 @@ Module Extended.
              | |- _ /\ _ => split
              | _ => solve [neq01]
              | _ => solve [eauto]
-             | _ => solve [intuition]
+             | _ => solve [intuition eauto]
              | _ => solve [etransitivity; eauto]
-             | |- Feq _ _ => field_algebra
-             | |- _ <> 0 => apply mul_nonzero_nonzero
-             | [ H : _ <> 0 |- _ <> 0 ] =>
-               intro; apply H;
-               field_algebra;
-               solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2
-                     | apply E.char_gt_2]
+             | |- _*_ <> 0 => apply mul_nonzero_nonzero
+             | [H: _ |- _ ] => solve [intro; apply H; super_nsatz]
+             | |- Feq _ _ => super_nsatz
              end.
 
     Obligation Tactic := bash.
@@ -63,8 +60,7 @@ Module Extended.
       (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _.
 
     Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q).
-    Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
-    Proof. typeclasses eauto. Qed.
+    Global Instance DecidableRel_eq : Decidable.DecidableRel eq := _.
 
     Local Hint Unfold from_twisted to_twisted eq : bash.