proposition: Lemma horner_derivE_wide n p x : (size p).-1 <= n -> horner tt (deriv tt p) x = \big[Rplus/R0]_(0 <= i < n) ((nth p i.+1) * (INR i.+1) * (x ^ i))%R.
proof: Proof. move=> H. rewrite (@hornerE_wide n); last by rewrite size_deriv. apply: eq_bigr => i _. congr Rmult. exact: coef_deriv. 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