proposition: Lemma horner_poly n E x : (\poly_(i < n) E i).[x] = \sum_(i < n) E i * x ^+ i.
proof: Proof. rewrite (@horner_coef_wide n) ?size_poly //. by apply: eq_bigr => i _; rewrite coef_poly ltn_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)