CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge

1 files changed, 4 insertions, 2 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 0afc07c5d..43787dd70 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -155,12 +155,14 @@ Module E.
       Proof.
         intros ? eq_zero.
         destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero.
-        destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra.
+        destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; super_nsatz.
       Qed.
 
       Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y).
       Proof.
-        unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero.
+        unfold solve_for_x2; simpl; split; intros H; pose proof a_d_y2_nonzero y.
+        - super_nsatz.
+        - rewrite H; clear H. super_nsatz.
       Qed.
     End PointCompression.
   End CompleteEdwardsCurveTheorems.