proposition: Lemma Pr_jcPr_gt0 E F : 0 < Pr P (E `* F) <-> 0 < \Pr_[E | F].
proof: Proof. split. - rewrite -{1}(setIT E) -{1}(setIT F) (setIC F) -setIX jcPrE. by move/Pr_cPr_gt0; rewrite -setTE -EsetT. - move=> H; rewrite -{1}(setIT E) -{1}(setIT F) (setIC F) -setIX. by apply/Pr_cPr_gt0; move: H; rewrite jcPrE -setTE -EsetT. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba