proposition: Lemma cauchy_seriesP {R : numFieldType} (V : normedModType R) (u_ : V ^nat) : cauchy (series u_ @ \oo) <-> forall e : R, e > 0 -> \forall n \near (\oo, \oo), `|\sum_(n.1 <= k < n.2) u_ k| < e.
proof: Proof. rewrite -cauchy_ballP; split=> su_cv _/posnumP[e]; have {}su_cv := !! su_cv _ (gt0 e); rewrite -near2_pair -ball_normE !near_simpl/= in su_cv *. apply: filterS su_cv => -[/= m n]; rewrite distrC sub_series. by have [|/ltnW]:= leqP m n => mn//; rewrite (big_geq mn) ?normr0. have := su_cv; rewrite near_swap => su_cvC; near=> m => /=; rewrite sub_series. by have [|/ltnW]:= leqP m.2 m.1 => m12; rewrite ?normrN; near: m. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau