proposition: Lemma map_comp_poly (aR rR : ringType) (f : {rmorphism aR -> rR}) p q : map_poly f (p \Po q) = map_poly f p \Po map_poly f q.
proof: Proof. elim/poly_ind: p => [|p a IHp]; first by rewrite !raddf0. rewrite comp_poly_MXaddC !rmorphD !rmorphM /= !map_polyC map_polyX. by rewrite comp_poly_MXaddC -IHp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)