proposition: Lemma poly_mult_0_r p q: poly_eq_zero q → poly_eq_zero (p * q).
proof: Proof. induction p as [|x p IH]; [easy|cbn]. intro eq0. apply poly_eq_zero_plus. - now apply poly_scalar_mult_0_r. - rewrite poly_eq_zero_cons; auto. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring