diff options
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 6 |
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. |