proposition: Lemma poly_negate_zero p: poly_eq_zero p ↔ poly_eq_zero (-p).
proof: Proof. induction p as [|x p IH]. { easy. } cbn. rewrite !poly_eq_zero_cons, IH. enough (x = 0 ↔ -x = 0) by tauto. split; intro eq0; ring [eq0]. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring