proposition: Lemma CV_radius_Reals_1 (a : nat -> R) (r : posreal) : CVN_r (fun n x => a n * x ^ n) r -> Rbar_le (Finite r) (CV_radius a).
proof: Proof. case => An [l [H H0]]. have H1 : is_lub_Rbar (CV_disk a) (CV_radius a). rewrite /CV_radius /Lub_Rbar ; by case: ex_lub_Rbar. have H2 : forall (y : R), 0 < y < r -> (CV_disk a y). move => y Hy. apply @ex_series_le with An. move => n ; rewrite /norm /= /abs /= Rabs_Rabsolu. apply H0 ; rewrite /Boule Rabs_pos_eq Rminus_0_r. by apply Hy. by apply Rlt_le, Hy. exists l. apply (is_lim_seq_spec _ l). intros eps. case: (H eps (cond_pos eps)) => N {} H. exists N => n Hn. set v := sum_n _ _. replace v with (sum_n (fun k : nat => Rabs (An k)) n). rewrite sum_n_Reals; by apply H. rewrite /v {v}. elim: n {Hn} => /= [ | n IH]. rewrite !sum_O ; apply Rabs_pos_eq. apply Rle_trans with (Rabs (a O * 0 ^ O)). by apply Rabs_pos. apply H0 ; rewrite /Boule Rminus_0_r Rabs_R0 ; by apply r. rewrite !sum_Sn IH Rabs_pos_eq. by []. apply Rle_trans with (Rabs (a (S n) * 0 ^ (S n))). by apply Rabs_pos. apply H0 ; rewrite /Boule Rminus_0_r Rabs_R0 ; by apply r. have H3 : forall y, 0 < y < r -> Rbar_le (Finite (y)) (CV_radius a). move => y Hy. by apply H1, H2. have H4 := CV_radius_ge_0 a. case: (CV_radius a) H3 H4 => /= [cv | | ] // H3 H4. apply Rnot_lt_le => /= H5. have H6 : 0 < (cv+r)/2 < r. lra. move: (H3 _ H6). lra. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series