proposition: Lemma Derive_n_coef (a : nat -> R) (n : nat) : Rbar_lt (Finite 0) (CV_radius a) -> Derive_n (PSeries a) n 0 = a n * (INR (fact n)).
proof: Proof. elim: n a => [ | n IH] a Ha. rewrite Rmult_1_r. rewrite /= /PSeries /Series -(Lim_seq_ext (fun _ => a O)). by rewrite Lim_seq_const. elim => /= [ | n IH]. rewrite sum_O ; ring. rewrite sum_Sn -IH /plus /= ; ring. simpl Derive_n. replace (Derive (Derive_n (PSeries a) n) 0) with (Derive_n (PSeries (PS_derive a)) n 0). rewrite IH. rewrite /fact -/fact mult_INR /PS_derive ; ring. by rewrite CV_radius_derive. transitivity (Derive_n (Derive (PSeries a)) n 0). apply Derive_n_ext_loc. case: (Rbar_eq_dec (CV_radius a) p_infty) => H. exists (mkposreal _ Rlt_0_1) => /= x Hx. apply sym_eq ; apply Derive_PSeries. by rewrite H. have Hc : 0 < real (CV_radius a). case: (CV_radius a) Ha H => /= [c | | ] Ha H ; by []. exists (mkposreal _ Hc) => /= x Hx. apply sym_eq ; apply Derive_PSeries. case: (CV_radius a) Hx Ha => /= [c | | ] Hx Ha //. by rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= -/(Rminus _ _) Rminus_0_r in Hx. move: (Derive_n_comp (PSeries a) n 1%nat 0) => /= ->. by replace (n+1)%nat with (S n) by ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series