proposition: Lemma is_series_Reals (a : nat -> R) (l : R) : is_series a l <-> infinite_sum a l.
proof: Proof. split => H. apply (is_lim_seq_spec _ l) in H. move => e He ; set eps := mkposreal e He. case: (H eps) => /= {H} N H. exists N => n Hn. rewrite <- sum_n_Reals. by apply (H n Hn). 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