proposition: Lemma iscvg_sum {I : eqType} (u : I -> nat -> R) r : (forall i, i \in r -> iscvg (u i)) -> iscvg (fun n => \sum_(i <- r) u i n).
proof: Proof. elim: r => [|i r ih] h. by exists 0; apply/(@ncvg_eq 0%:S)/ncvgC => n; rewrite big_nil. case: ih => [j jr|c cv]; first by apply/h; rewrite inE jr orbT. have [l cl]: iscvg (u i) by apply/h; rewrite inE eqxx. exists (c + l); have := ncvgD cv cl; apply/ncvg_eq. by move=> n; rewrite big_cons addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology