proposition: Lemma ex_series_Cauchy {K : AbsRing} {V : CompleteNormedModule K} (a : nat -> V) : Cauchy_series a -> ex_series a.
proof: Proof. intros Ca. destruct (proj1 (filterlim_locally_cauchy (U := V) (F := eventually) (sum_n a))) as [l Hl]. 2: now exists l. intros eps. destruct (Ca eps) as [N HN]. exists (le N). split. now exists N. intros u v. wlog Huv: u v / (u <= v)%nat. intros H. destruct (Nat.le_gt_cases u v) as [Huv|Huv]. now apply H. intros Hu Hv. apply ball_sym. apply H => //. now apply Nat.lt_le_incl. intros Hu Hv. apply: norm_compat1. rewrite -(sum_n_m_sum_n _ _ _ Huv). apply HN => //. now apply le_S. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy