proposition: Lemma CV_radius_ge_0 (a : nat -> R) : Rbar_le (Finite 0) (CV_radius a).
proof: Proof. rewrite /CV_radius /Lub_Rbar ; case: ex_lub_Rbar => /= l Hl. apply Hl, CV_disk_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series