proposition: Lemma CV_disk_scal_r (c : R) (a : nat -> R) (x : R) : (CV_disk a x) -> (CV_disk (PS_scal_r c a) x).
proof: Proof. move => Ha. apply ex_series_ext with (fun n => Rabs c * Rabs (a n * x ^ n)). move => n ; rewrite -Rabs_mult ; apply f_equal ; rewrite /PS_scal_r /= ; ring. by apply @ex_series_scal ; apply Ha. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series