proposition: Lemma pe2e_lem1: forall x1 y1 z1 (H1 : y1 ^ 2 * z1 = x1 ^ 3 + A * x1 * z1 ^ 2 + B * z1 ^ 3) (Hb: is_zero z1 = false), (y1 / z1) ^ 2 = (x1 / z1) ^ 3 + A * (x1 / z1) + B.
proof: Proof. intros x1 y1 z1 H1 Hb. field [H1]. intros H3; case (Eth.(is_zero_correct) z1); intros _ H4. generalize (H4 H3); rewrite Hb; intros; discriminate. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith