proposition: Lemma ex_series_lim_0 (a : nat -> R) : ex_series a -> is_lim_seq a 0.
proof: Proof. intros Hs. apply is_lim_seq_spec. intros eps. apply (Cauchy_ex_series (V := R_CompleteNormedModule)) in Hs. case: (Hs eps) => {Hs} N Hs. exists (S N) ; case => [ | n] Hn. by apply Nat.nle_succ_0 in Hn. apply le_S_n in Hn. replace (a (S n) - 0) with (sum_n_m a (S n) (S n)). apply Hs ; by intuition. by rewrite sum_n_n Rminus_0_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy