proposition: Lemma total_prob_cond : Pr d E = \sum_(i in I) `Pr_[E | F i] * Pr d (F i).
proof: Proof. rewrite (total_prob _ _ _ dis cov); apply eq_bigr; move=> i _. by rewrite product_rule. 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