proposition: Lemma horner_coef_wide n p x : size p <= n -> p.[x] = \sum_(i < n) p`_i * x ^+ i.
proof: Proof. move=> le_p_n. rewrite horner_coef (big_ord_widen n (fun i => p`_i * x ^+ i)) // big_mkcond. by apply: eq_bigr => i _; case: ltnP => // le_p_i; rewrite nth_default ?simp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)