proposition: Lemma Boole_eq (I : finType) (F : I -> {set A}) : (forall i j, i != j -> [disjoint F i & F j]) -> Pr (\bigcup_(i in I) F i) = \sum_(i in I) Pr (F i).
proof: Proof. move=> H. rewrite (reindex_onto enum_val enum_rank) /=; last first. by move=> *; exact: enum_rankK. rewrite [in RHS](reindex_onto enum_val enum_rank) /=; last first. by move=> *; exact: enum_rankK. rewrite (eq_bigl xpredT); last by move=> i; rewrite enum_valK eqxx. rewrite Pr_big_union_disj; last first. move=> i j ij. suff : enum_val i != enum_val j by move/H. by apply: contra ij => /eqP/enum_val_inj ->. by rewrite [in RHS](eq_bigl xpredT) // => i; rewrite enum_valK eqxx. 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