proposition: Lemma dfsume_ge0 (I : choiceType) (P : set I) (F : I -> \bar^d R) : (forall i, P i -> 0 <= F i) -> 0 <= \sum_(i \in P) F i.
proof: Proof. move=> PF; case: finite_supportP; rewrite ?big_nil// => X XP F0 _. by rewrite big_seq_cond big_mkcondr dsume_ge0// => i /XP/PF. 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