proposition: Lemma map_comp_poly (aR : fieldType) (rR : idomainType) (f : {rmorphism aR -> rR}) (p q : {poly aR}) : (p \Po q) ^ f = (p ^ f) \Po (q ^ f).
proof: Proof. rewrite !comp_polyE size_map_poly; apply: (big_ind2 (fun x y => x ^ f = y)). + by rewrite rmorph0. + by move=> u u' v v' /=; rewrite rmorphD /= => -> ->. move=> /= i _; rewrite -mul_polyC rmorphM /= map_polyC mul_polyC. by rewrite coef_map rmorphX. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)