proposition: Lemma PSeries_continuity (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> continuity_pt (PSeries a) x.
proof: Proof. move => H. case: (CV_radius_Reals_2 a x H) => r H0. apply (CVU_continuity (fun (n : nat) (x : R) => sum_f_R0 (fun k : nat => a k * x ^ k) n) (PSeries a) x r H0). move => n y Hy. apply continuity_pt_finite_SF. move => k Hk. apply continuity_pt_scal. elim: k {Hk} => /= [ | k IH]. by apply continuity_pt_const => d f. apply continuity_pt_mult. apply derivable_continuous_pt, derivable_pt_id. by apply IH. rewrite /Boule Rminus_eq_0 Rabs_R0 ; by apply r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series