proposition: Lemma cvg_series_cvg_series_group (R : realFieldType) (f : R ^nat) k : cvg (series f @ \oo) -> (0 < k)%N -> [series \sum_(n * k <= i < n.+1 * k) f i]_n @ \oo --> lim (series f @ \oo).
proof: Proof. move=> /cvg_ballP cf k0; apply/cvg_ballP => _/posnumP[e]. have := !! cf _ (gt0 e) => -[n _ nl]; near=> m. rewrite /ball /= [in X in `|_ - X|]/series [in X in `|_ - X|]/= -big_nat_mul. have /nl : (n <= m * k)%N. by near: m; exists n.+1 => //= p /ltnW /leq_trans /(_ (leq_pmulr _ k0)). by rewrite /ball /= distrC. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp