proposition: Lemma CV_disk_correct (a : nat -> R) (x : R) : CV_disk a x -> ex_pseries a x.
proof: Proof. intros H; apply ex_series_Rabs. apply ex_series_ext with (2:=H). intros n; apply f_equal. now rewrite Rmult_comm pow_n_pow. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series