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