proposition: Lemma to_poly_scale_r a p : to_poly (map_hpoly (fun x => (x * a)%C) p) = to_poly p * a%:P.
proof: Proof. elim: p=> [b|b n p ih] /=; rewrite /mul_op /mulA polyCM //. by rewrite ih mulrDl -mulrA mulXnC -mulrA. 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)