proposition: Lemma to_poly_scale_l a p : to_poly (a *: p)%C = a *: (to_poly p).
proof: Proof. elim: p=> [b|b n p ih] /=; rewrite /mul_op /mulA -mul_polyC polyCM //. by rewrite ih -mul_polyC mulrDr mulrA /mul_op /mulA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)