proposition: Lemma Rderive_delta (Pr : R -> Prop) (n : nat) (x0 : R) : dom x0 -> Pr x0 -> Rderive_over (fun t => dom t /\ Pr t) (Rdelta n x0) (Rdelta' n x0).
proof: Proof. move=> Dx0 HPr x Hx. rewrite /Rdelta /Rdelta'. apply: is_derive_minus. apply: Derive_correct. now apply (Hder_n 1). set d := (_ ^`()).[_]. have->: d = scal R1 d by rewrite /scal /= /mult /= Rmult_1_l. apply: is_derive_comp; last first. rewrite -[R1]Rminus_0_r; apply: is_derive_minus; by auto_derive. rewrite /d. exact: PolR.is_derive_horner. 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