proposition: Lemma lim_series_le (V : realFieldType) (f g : V ^nat) : cvgn (series f) -> cvgn (series g) -> (forall n, f n <= g n) -> limn (series f) <= limn (series g).
proof: Proof. by move=> cf cg fg; apply: (ler_lim cf cg); near=> x; rewrite ler_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