proposition: Lemma poly_mult_0_l p q: poly_eq_zero p → poly_eq_zero (p * q).
proof: Proof. induction 1 using poly_eq_zero_ind; [easy|cbn]. apply poly_eq_zero_plus. - now apply poly_scalar_mult_0_l. - rewrite poly_eq_zero_cons; auto. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring