proposition: Lemma ex_derive_n_PSeries (n : nat) (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> ex_derive_n (PSeries a) n x.
proof: Proof. elim: n a x => [ | n IH] a x Hx. by simpl. simpl. exists (PSeries (PS_derive_n (S n) a) x). by apply (is_derive_n_PSeries (S n)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series