proposition: Lemma poly_scalar_mult_0_r q c: poly_eq_zero q → poly_eq_zero (c · q).
proof: Proof. induction q as [|x q IH]. { easy. } cbn. rewrite !poly_eq_zero_cons. intros [-> ?]; split; auto. ring. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring