proposition: Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) : cvgn [normed series u_] -> cvgn (series u_).
proof: Proof. move=> /cauchy_cvgP/cauchy_seriesP u_ncvg. apply/cauchy_cvgP/cauchy_seriesP => e /u_ncvg. apply: filterS => n /=; rewrite ger0_norm ?sumr_ge0//. by apply: le_lt_trans; apply: ler_norm_sum. 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