proposition: Lemma ex_derive_PSeries (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> ex_derive (PSeries a) x.
proof: Proof. move => Hx ; exists (PSeries (PS_derive a) x). by apply is_derive_PSeries. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series