proposition: Lemma ex_series_Reals_0 (a : nat -> R) : ex_series a -> { l:R | Un_cv (fun N:nat => sum_f_R0 a N) l }.
proof: Proof. move => H ; exists (Series a) ; case: H => l H. replace (Series a) with l. move => e He ; set eps := mkposreal e He. apply (is_lim_seq_spec _ l) in H. case: (H eps) => /= {H} N H. exists N => n Hn. rewrite <- sum_n_Reals. by apply (H n Hn). apply sym_eq. rewrite /Series. replace l with (real (Finite l)) by auto. apply f_equal. by apply is_lim_seq_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy