proposition: Lemma popp_lem: forall x y z, y ^ 2 * z = x ^ 3 + A * x * z ^ 2 + B * z ^ 3 -> (- y) ^ 2 * z = x ^ 3 + A * x * z ^ 2 + B * z ^ 3.
proof: Proof. intros x1 y1 z1 H; rewrite <- H; simpl; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith