proposition: Lemma hornerE p x : horner tt p x = \big[Rplus/0%R]_(0 <= i < size p) Rmult (nth p i) (x ^ i).
proof: Proof. elim: p; first by rewrite big_mkord big_ord0 /=. move=> t p /= ->. rewrite big_nat_recl // pow_O /=. rewrite Rmult_1_r Rplus_comm. case: (size p)=> [|n]. by rewrite !big_mkord !big_ord0 /= Rmult_0_l. rewrite Rmult_comm big_distrr /=; congr Rplus. apply: eq_bigr => i _. by rewrite ![Rmult x _]Rmult_comm Rmult_assoc. 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