proposition: Lemma CV_radius_Reals_2 (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> exists r : posreal, CVU (fun n x => sum_f_R0 (fun k => a k * x ^ k) n) (PSeries a) x r.
proof: Proof. move => Hx. have H : exists r : posreal, Rabs x < r /\ Rbar_lt (Finite r) (CV_radius a). case: (CV_radius a) Hx => /= [cv | | ] Hx. have H : 0 < (Rabs x + cv)/2. generalize (Rabs_pos x) ; lra. exists (mkposreal _ H) => /=. lra. have H : 0 < Rabs x + 1. apply Rle_lt_0_plus_1, Rabs_pos. exists (mkposreal _ H) => /=. split. by apply Rlt_plus_1. by []. by []. case: H => r H. apply CVN_CVU_r with r. by apply CV_radius_Reals_0, H. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series