proposition: Lemma total_prob (I : finType) (E : {set A}) (F : I -> {set A}) : (forall i j, i != j -> [disjoint F i & F j]) -> cover (F @: I) = [set: A] -> Pr E = \sum_(i in I) Pr (E :&: F i).
proof: Proof. move=> dis cov; have {1}-> : E = \bigcup_(i in I) (E :&: F i). by rewrite cover_imset in cov; rewrite -big_distrr /= cov setIT. rewrite Boole_eq // => i j /dis; rewrite -2!setI_eq0 -setIIr => /eqP ->. by rewrite setI0. 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