proposition: Lemma is_pseries_derive (a : nat -> R) x : Rbar_lt (Rabs x) (CV_radius a) -> is_pseries (PS_derive a) x (Derive (PSeries a) x).
proof: Proof. intros Hx. assert (Ha := is_derive_PSeries _ _ Hx). apply is_derive_unique in Ha. rewrite Ha. apply PSeries_correct. by apply CV_radius_inside ; rewrite CV_radius_derive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series