proposition: Lemma Cauchy_ex_series {K : AbsRing} {V : CompleteNormedModule K} (a : nat -> V) : ex_series a -> Cauchy_series a.
proof: Proof. intros [l Hl] eps. generalize (filterlim_locally_closely (U := V) (F := eventually) (sum_n (fun k => a k))). move /proj2 /(_ (ex_intro _ l Hl)). move /(filterlim_filter_le_2 _ closely_le_closely_norm). move /filterlim_closely_norm. case /(_ eps) => [P [[N HN] HP]]. exists (S N). intros [|u] v Hu Hv. elim Nat.nle_succ_0 with (1 := Hu). destruct (Nat.le_gt_cases u v) as [Huv|Huv]. rewrite (sum_n_m_sum_n _ _ _ Huv). apply HP ; apply HN. now apply le_S_n. now apply Nat.lt_le_incl. rewrite sum_n_m_zero. rewrite norm_zero. apply cond_pos. now apply Nat.lt_lt_succ_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy