proposition: Fact horner_eval_is_multiplicative x : multiplicative (horner_eval x).
proof: Proof. have cxid: commr_rmorph idfun x by apply: mulrC. have evalE : horner_eval x =1 horner_morph cxid. by move=> p; congr _.[x]; rewrite map_poly_id. by split=> [p q|]; rewrite !evalE ?rmorph1// rmorphM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)