proposition: Lemma CV_radius_scal_r (c : R) (a : nat -> R) : c <> 0 -> (CV_radius (PS_scal_r c a)) = (CV_radius a).
proof: Proof. intros Hc. rewrite -(CV_radius_scal c a). apply CV_radius_ext => n. apply Rmult_comm. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series