proposition: Lemma Derive_n_PSeries (n : nat) (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> Derive_n (PSeries a) n x = PSeries (PS_derive_n n a) x.
proof: Proof. move => H. apply is_derive_n_unique. by apply is_derive_n_PSeries. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series