proposition: Lemma dfsume_gt0 (I : choiceType) (P : set I) (F : I -> \bar^d R) : 0 < \sum_(i \in P) F i -> exists2 i, P i & 0 < F i.
proof: Proof. rewrite dual_fsumeE oppe_gt0 => /fsume_lt0[i Pi]. by rewrite oppe_lt0 => ?; exists i. 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