proposition: Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) : (forall n, P n -> 0 <= a n) -> \sum_(i <oo | P i) a i = \esum_(i in [set x | P x]) a i.
proof: Proof. move=> a0; apply/eqP; rewrite eq_le; apply/andP; split. apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n. apply: ereal_sup_ub => /=; exists [set` [fset val i | i in 'I_n & P i]%fset]. split; first exact: finite_fset. by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. rewrite fsbig_finite//= set_fsetK big_imfset/=; last by move=> ? ? ? ? /val_inj. by rewrite big_filter big_enum_cond/= big_mkord. apply: ub_ereal_sup => _ [/= F [finF PF] <-]. rewrite fsbig_finite//= -(big_rmcond_in P)/=; first exact: lee_sum_fset_lim. by move=> k; rewrite in_fset_set// inE => /PF ->. 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