proposition: Lemma lim_series_norm {R : realType} (V : completeNormedModType R) (f : V ^nat) : cvgn [normed series f] -> `|limn (series f)| <= limn [normed series f].
proof: Proof. move=> cnf; have cf := normed_cvg cnf. rewrite -lim_norm // (ler_lim (is_cvg_norm cf) cnf) //. by near=> x; rewrite ler_norm_sum. 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