proposition: Lemma Pr_cPr_gt0 E F : 0 < Pr d (E :&: F) <-> 0 < `Pr_[E | F].
proof: Proof. rewrite Pr_gt0; split => H; last first. by move/cPr_gt0 : H; apply: contra => /eqP; rewrite /cPr => ->; rewrite div0R. rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0 //. by apply: contra H; rewrite setIC => /eqP F0; apply/eqP/Pr_domin_setI. 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