proposition: Lemma summable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) : (forall i, P i -> 0 <= f i)%E -> summable P f -> \sum_(i <oo | P i) f i = (lim ((fun n => (\sum_(0 <= k < n | P k) fine (f k))%R) @ \oo))%:E.
proof: Proof. move=> f0 Pf; pose A_ n := (\sum_(0 <= k < n | P k) fine (f k))%R. transitivity (lim (EFin \o A_ @ \oo)). apply/congr_lim/funext => /= n; rewrite /A_ /= -sumEFin. apply eq_bigr => i Pi/=; rewrite fineK//. by rewrite fin_num_abs (@summable_pinfty _ _ P). by rewrite EFin_lim//; apply: summable_cvg. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun