proposition: Lemma poppe_lem 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. by rewrite sqrrN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)