proposition: Lemma cvg_nnesum (J : Type) (r : seq J) (f : J -> I -> \bar R) (l : J -> \bar R) (P : pred J) : (forall j, P j -> \near F, 0 <= f j F) -> (forall j, P j -> f j @ F --> l j) -> \sum_(j <- r | P j) f j i @[i --> F] --> \sum_(j <- r | P j) l j.
proof: Proof. pose bigsimp := (big_nil, big_cons); elim: r => [|x r IHr]/= f0 fl; rewrite bigsimp; under eq_fun do rewrite bigsimp. exact: cvg_cst. case: ifPn => [Px|Pnx]; last exact: IHr. apply: cvgeD; [|exact: fl|exact: IHr]. by rewrite ge0_adde_def ?inE// ?sume_ge0// => [|j Pj]; rewrite (cvge_ge _ (fl _ _))//; apply: f0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule