proposition: Lemma CV_disk_scal (c : R) (a : nat -> R) (x : R) : (CV_disk a x) -> (CV_disk (PS_scal 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 ; by rewrite /PS_scal /= Rmult_assoc. apply @ex_series_scal. by apply Ha. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series