proposition: Lemma cPr_1 (U : finType) (P : {fdist U}) (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) a : `Pr[X = a] != 0 -> \sum_(b <- fin_img Y) `Pr[ Y = b | X = a ] = 1.
proof: Proof. rewrite -pr_eq_set1 pr_inE' Pr_set1 -{1}(fst_RV2 _ Y) => Xa0. set Q := `p_[% X, Y] `(| a ). rewrite -[RHS](FDist.f1 Q) [in RHS](bigID (mem (fin_img Y))) /=. rewrite [X in _ = _ + X](eq_bigr (fun=> 0)); last first. move=> b bY. rewrite /Q jfdist_condE // /jcPr /Pr !(big_setX,big_set1) /= fdistXE fdistX2 fst_RV2. rewrite -!pr_eqE' !pr_eqE. rewrite /Pr big1 ?div0R // => u. rewrite inE => /eqP[Yub ?]. exfalso. move/negP : bY; apply. by rewrite mem_undup; apply/mapP; exists u => //; rewrite mem_enum. rewrite big_const iter_addR mulR0 addR0. rewrite big_uniq; last by rewrite /fin_img undup_uniq. apply eq_bigr => b; rewrite mem_undup => /mapP[u _ bWu]. rewrite /Q jfdist_condE // fdistX_RV2. by rewrite jcPrE -cpr_inE' cpr_eq_set1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba