proposition: Lemma ex_derive_big I (s : seq I) : forall (f : I -> R -> R) (x : R), (forall k : I, ex_derive (f k) x) -> ex_derive (fun x0 : Rdefinitions.R => \big[Rplus/0]_(i <- s) f i x0) x.
proof: Proof. move => f x Hf. elim: s => [ | a b Hrec] => /= . apply: (ex_derive_ext (fun x0 => 0)) => [t|]; first by rewrite big_nil. apply: ex_derive_const. apply: (ex_derive_ext (fun t => f a t + \big[Rplus/0]_(j <- b) f j t)). by move => t; rewrite big_cons. apply: ex_derive_plus. by apply: Hf. by apply: Hrec. 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