proposition: Fact horner_is_multiplicative : multiplicative (horner_morph cfu).
proof: Proof. split=> [p q|]; last by rewrite /horner_morph rmorph1 hornerC. rewrite /horner_morph rmorphM /= hornerM_comm //. by apply: comm_coef_poly => i; rewrite coef_map cfu. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)