proposition: Fact map_poly_is_multiplicative : multiplicative (map_poly f).
proof: Proof. split=> [p q|]; apply/polyP=> i; last first. by rewrite !(coef_map, coef1) /= rmorph_nat. rewrite coef_map /= !coefM /= !rmorph_sum; apply: eq_bigr => j _. by rewrite !coef_map rmorphM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)