proposition: Lemma bigXadd'_P (m n : nat) (x0 s : R) : dom x0 -> ex_derive_n f0 n x0 -> m <= n -> \big[Rplus/R0]_(0 <= i < m) (PolR.nth (P x0 n) i.+1 * INR i.+1 * s ^ i)%R = \big[Rplus/R0]_(0 <= i < m) ((Dn i.+1 x0) / INR (fact i) * s ^ i)%R.
proof: Proof. move=> H0 Hx0 Hmn; rewrite !big_mkord. case: m Hmn =>[|m] Hmn; first by rewrite !big_ord0. elim/big_ind2: _ =>[//|x1 x2 y1 y2 -> ->//|i _]. rewrite Poly_nth //; last by case: i => [i Hi] /=; exact: leq_trans Hi Hmn. rewrite fact_simpl mult_INR. field. split; by [apply: INR_fact_neq_0 | apply: not_0_INR ]. 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