proposition: Lemma CV_disk_inside (a : nat -> R) (x : R) : Rbar_lt (Finite (Rabs x)) (CV_radius a) -> ex_series (fun n => Rabs (a n * x ^ n)).
proof: Proof. move => Ha. assert (H : ~ ~ ex_series (fun n => Rabs (a n * x ^ n))). contradict Ha. apply Rbar_le_not_lt. rewrite /CV_radius /Lub_Rbar ; case: ex_lub_Rbar => l /= [ub lub]. apply: lub => r Hr. apply Rnot_lt_le ; contradict Ha. move: Hr. apply CV_disk_le. by apply Rlt_le, Rlt_le_trans with (2 := Rle_abs _). by case: (ex_series_dec (fun n => Rabs (a n * x ^ n))). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series