proposition: Lemma Pr_set0P E : Pr E = 0 <-> (forall a, a \in E -> P a = 0).
proof: Proof. rewrite /Pr (eq_bigl (fun x => x \in E)) //; split => [|h]. move/eqP; rewrite psumr_eq0// => /allP + a aE. by move/(_ a); rewrite mem_index_enum aE implyTb => /(_ isT)/eqP. apply/eqP; rewrite psumr_eq0 //; apply/allP => a _. by apply/implyP => /h/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist