proposition: Fact comp_poly_multiplicative q : multiplicative (comp_poly q).
proof: Proof. split=> [p1 p2|]; last by rewrite comp_polyC. by rewrite /comp_poly rmorphM hornerM_comm //; apply: mulrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)