proposition: Lemma ex_series_Reals_1 (a : nat -> R) : { l:R | Un_cv (fun N:nat => sum_f_R0 a N) l } -> ex_series a.
proof: Proof. case => l H. exists l. apply (is_lim_seq_spec _ l). move => eps. case: (H eps (cond_pos eps)) => {H} N H. exists N => n Hn. rewrite sum_n_Reals. by apply (H n Hn). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy