proposition: Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) : (forall i, P i -> 0 <= f i)%E -> summable P f -> cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo).
proof: Proof. move=> f0 Pf; apply: nondecreasing_is_cvgn. by apply: nondecreasing_series => n Pn; exact/fine_ge0/f0. exists (fine (\sum_(i <oo | P i) `|f i|)) => x /= [n _ <-]. rewrite summable_fine_sum// -lee_fin fineK//; last first. by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (summable_pinfty Pf). rewrite fineK//; last first. rewrite nneseries_esum// fin_numElt; apply/andP; split. by rewrite (@lt_le_trans _ _ 0)// ?lte_ninfty//; exact: esum_ge0. by apply: le_lt_trans Pf; apply le_esum. apply: le_trans (nneseries_lim_ge n _) => //; apply: lee_sum => i _. by rewrite lee_abs. 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