proposition: Lemma is_cvg_series_restrict u_ : cvgn [sequence \sum_(N <= k < n) u_ k]_n = cvgn (series u_).
proof: Proof. suff -> : (fun n => \sum_(N <= k < n) u_ k) = fun n => if (n <= N)%N then \sum_(N <= k < n) u_ k else series u_ n - \sum_(0 <= k < N) u_ k. by rewrite is_cvg_restrict/= is_cvgDlE//; apply: is_cvg_cst. rewrite funeqE => n; case: leqP => // ltNn; apply: (canRL (addrK _)). by rewrite seriesEnat addrC -big_cat_nat// ltnW. 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