proposition: Lemma horner_map p x : p^f.[f x] = f p.[x].
proof: Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !(rmorph0, horner0). rewrite hornerMXaddC !rmorphD !rmorphM /=. by rewrite map_polyX map_polyC hornerMXaddC IHp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)