proposition: Lemma Pr_domin_setI (A : finType) (d : {fdist A}) (E F : {set A}) : Pr d E = 0 -> Pr d (E :&: F) = 0.
proof: Proof. move=> PE0; apply/eqP; rewrite psumr_eq0//; apply/allP => a _. apply/implyP; rewrite inE => /andP[aE aF]. move/eqP : PE0; rewrite psumr_eq0// => /allP. by move=> /(_ a); rewrite mem_index_enum => /(_ isT); rewrite aE implyTb. 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