proposition: Lemma is_derive_n_PSeries (n : nat) (a : nat -> R) : forall x, Rbar_lt (Rabs x) (CV_radius a) -> is_derive_n (PSeries a) n x (PSeries (PS_derive_n n a) x).
proof: Proof. elim: n => [ | n IH] x Hx. simpl ; rewrite /PS_derive_n /=. apply PSeries_ext => n. rewrite -plus_n_O. field. apply Rgt_not_eq. by apply INR_fact_lt_0. simpl ; rewrite /PS_derive_n /=. apply is_derive_ext_loc with (PSeries (fun k : nat => INR (fact (k + n)) / INR (fact k) * a (k + n)%nat)). case Ha : (CV_radius a) => [cva | | ]. move: (Hx) ; rewrite Ha ; move/Rminus_lt_0 => Hx0. exists (mkposreal _ Hx0) => /= y Hy. apply sym_eq. apply is_derive_n_unique. apply IH. rewrite Ha /=. replace y with ((y-x) + x) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). by apply Rlt_minus_r. exists (mkposreal _ Rlt_0_1) => /= y Hy. apply sym_eq. apply is_derive_n_unique. apply IH. by rewrite Ha /=. by rewrite Ha in Hx. evar (l : R). replace (PSeries _ x) with l. rewrite /l {l}. apply is_derive_PSeries. replace (CV_radius (fun k : nat => INR (fact (k + n)) / INR (fact k) * a (k + n)%nat)) with (CV_radius a). by apply Hx. elim: n {IH} => [ | n IH]. apply CV_radius_ext => n. rewrite -plus_n_O. field. apply Rgt_not_eq. by apply INR_fact_lt_0. rewrite IH. rewrite -CV_radius_derive. apply CV_radius_ext => k. rewrite /PS_derive. rewrite -plus_n_Sm plus_Sn_m /fact -/fact ?mult_INR ?S_INR. field. rewrite -S_INR ; split ; apply Rgt_not_eq. by apply INR_fact_lt_0. apply (lt_INR O), Nat.lt_0_succ. rewrite /l {l}. apply PSeries_ext. move => k ; rewrite /PS_derive. rewrite -plus_n_Sm plus_Sn_m /fact -/fact ?mult_INR ?S_INR. field. rewrite -S_INR ; split ; apply Rgt_not_eq. by apply INR_fact_lt_0. apply (lt_INR O), Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series