proposition: Lemma Cauchy_series_Reals (a : nat -> R) : Cauchy_series a <-> Cauchy_crit_series a.
proof: Proof. split => Hcv. apply cv_cauchy_1, ex_series_Reals_0. by apply: ex_series_Cauchy. apply: Cauchy_ex_series. apply ex_series_Reals_1. apply cv_cauchy_2. by apply Hcv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy