proposition: Lemma jtotal_prob_cond : Pr P`1 E = \sum_(i in I) \Pr_[E | F i] * Pr P`2 (F i).
proof: Proof. rewrite -Pr_XsetT -EsetT. rewrite (@total_prob_cond _ _ _ _ (fun i => T`* F i)); last 2 first. - move=> i j ij; rewrite -setI_eq0 !setTE setIX setTI. by move: (dis ij); rewrite -setI_eq0 => /eqP ->; rewrite setX0. - apply/setP => -[a b]; rewrite inE /cover. apply/bigcupP => /=. move: cov; rewrite /cover => /setP /(_ b). rewrite !inE => /bigcupP[b']. move/imsetP => [i _ ->{b'} bFi]. exists (T`* F i). by apply/imsetP; exists i. by rewrite inE. by apply eq_bigr => i _; rewrite -Pr_setTX -setTE; congr (_ * _); rewrite jcPrE. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba