proposition: Lemma is_derive_horner p x : is_derive (horner tt p) x (horner tt (deriv tt p) x).
proof: Proof. elim: p => [|a p IHp]. - rewrite /horner /=; exact: is_derive_const. - apply: (@is_derive_ext _ _ (fun x => horner tt p x * x + a)%R); first done. rewrite -[horner _ _ _]Rplus_0_r. apply: is_derive_plus; last by auto_derive. suff->: horner tt (deriv tt (a :: p)) x = ((horner tt (deriv tt p) x) * x + (horner tt p x) * 1)%R. apply: is_derive_mult =>//. apply: is_derive_id. exact: Rmult_comm. rewrite (@horner_derivE_wide (size p)) // (@horner_derivE_wide (size p).-1) // (@hornerE_wide (size p)) //. rewrite Rmult_1_r. rewrite big_distrl. case E: (size p) => [|sp]; first by rewrite !(big_mkord, big_ord0) Rplus_0_l. rewrite [LHS]big_ltn // [in LHS]big_add1. rewrite [in X in _ = (_ + X)%R](big_ltn, big_add1) //. rewrite [in RHS]Rplus_comm [in RHS]Rplus_assoc; congr Rplus. by rewrite !Rmult_1_r. rewrite big_add1. rewrite -big_split. apply: eq_bigr => i _. have->: INR i.+2 = (INR i.+1 + 1)%R by []. have->: nth (a :: p) i.+2 = nth p i.+1 by []. rewrite -tech_pow_Rmult; simpl; ring. 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