proposition: Lemma hornerE_wide n p x : size p <= n -> horner tt p x = \big[Rplus/R0]_(0 <= i < n) Rmult (nth p i) (x ^ i).
proof: Proof. move=> Hn; rewrite hornerE (big_nat_leq_idx _ Hn) //. by move=> i /andP [Hi _]; rewrite nth_default // Rmult_0_l. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec