proposition: Lemma scale_toC (p : {poly R}) (a : R) : toC (p \scale a) = (toC p) \scale a%:C.
proof: Proof. by rewrite /scaleX_poly (map_comp_poly _ p ('X * a%:P)) rmorphM /= map_polyX map_polyC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)