proposition: Lemma pfsume_eq0 (I : choiceType) (P : set I) (F : I -> \bar R) : finite_set P -> (forall i, P i -> 0 <= F i) -> \sum_(i \in P) F i = 0 -> forall i, P i -> F i = 0.
proof: Proof. move=> Pfin F0 /eqP; apply: contraTP => /existsPNP[i Pi /eqP Fi0]. rewrite (fsbigD1 i)//= padde_eq0 ?F0 ?negb_and ?Fi0//. by rewrite fsume_ge0// => j [/F0->]. 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