proposition: Lemma Rpol_derive p (c : R) (x : R) : Derive (PolR.horner tt (PolR.primitive tt c p)) x = PolR.horner tt p x.
proof: Proof. have derMonom : forall k : nat, ex_derive (fun y : R => PolR.nth (PolR.primitive tt c p) k.+1 * powerRZ y (Z.of_nat k.+1)) x. move => k. apply: ex_derive_mult. apply: ex_derive_const. apply: (ex_derive_ext (fun x => x ^ (k.+1))). by move => t; rewrite -pow_powerRZ. apply: ex_derive_pow; apply: ex_derive_id. rewrite PolR.hornerE. rewrite (Derive_ext _ _ _ (horner_primitive c p)). set X := RHS. have -> : X = 0 + X by rewrite Rplus_0_l. rewrite Derive_plus; [ |by apply: ex_derive_const |]. - congr (_ + _); first by apply: Derive_const. rewrite derive_big. rewrite [LHS]big_nat_cond /X [RHS]big_nat_cond. apply: eq_bigr => i; rewrite andbT => Hi. rewrite Derive_mult. have -> : Derive (fun _ : R => PolR.nth (PolR.primitive tt c p) i.+1) x = 0. by apply: Derive_const. ring_simplify. rewrite (Derive_ext _ (fun x => x ^ (i.+1))); last first. by move => t; rewrite -pow_powerRZ. rewrite PolR.nth_primitive ifF /PolR.int_coeff => //. rewrite Derive_pow ?Derive_id -?pred_Sn. field. apply: not_0_INR => // . exact: ex_derive_id. by apply/negbTE; rewrite -leqNgt; case/andP: Hi. apply: ex_derive_const. apply: (ex_derive_ext (fun x => x ^ (i.+1))). by move => t; rewrite -pow_powerRZ. apply: ex_derive_pow; apply: ex_derive_id. by []. by apply: ex_derive_big. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound