proposition: Lemma CV_disk_plus (a b : nat -> R) (x : R) : (CV_disk a x) -> (CV_disk b x) -> (CV_disk (PS_plus a b) x).
proof: Proof. move => Ha Hb. move: (ex_series_plus _ _ Ha Hb). apply @ex_series_le => n ; rewrite /norm /= /abs /= Rabs_Rabsolu. rewrite Rmult_plus_distr_r. by apply Rabs_triang. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series