proposition: Lemma poly_mult_cons_r p q x: p * (x::q) = x · p + (0 :: p * q).
proof: Proof. induction p as [|y p IH]; cbn; auto. split; auto. rewrite IH, !associativity, (commutativity (y · q)). split; try easy. ring. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring