proposition: Lemma fsume_lt0 (I : choiceType) (P : set I) (F : I -> \bar R) : \sum_(i \in P) F i < 0 -> exists2 i, P i & F i < 0.
proof: Proof. apply: contraPP => /forall2NP xNPF; rewrite le_gtF// fsume_ge0// => i Pi. by case: (xNPF i) => // /negP; case: ltP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal