proposition: Lemma CV_radius_scal (c : R) (a : nat -> R) : c <> 0 -> (CV_radius (PS_scal c a)) = (CV_radius a).
proof: Proof. rewrite /CV_radius /Lub_Rbar ; case: ex_lub_Rbar => la [ub_a lub_a] ; case: ex_lub_Rbar => lc [ub_c lub_c] /= Hc. apply Rbar_le_antisym. apply lub_a => x Hx. apply ub_c. assert (CV_disk (PS_scal (/c) (PS_scal c a)) x). by apply CV_disk_scal. move: H ; apply ex_series_ext => n. apply f_equal. rewrite /PS_scal /scal /= /mult /= ; by field. apply lub_c => x Hx. apply ub_a. by apply CV_disk_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series