proposition: Lemma horner_coef p x : p.[x] = \sum_(i < size p) p`_i * x ^+ i.
proof: Proof. rewrite /horner. elim: {p}(p : seq R) => /= [|a s ->]; first by rewrite big_ord0. rewrite big_ord_recl simp addrC big_distrl /=. by congr (_ + _); apply: eq_bigr => i _; rewrite -mulrA exprSr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)