proposition: Lemma inde_events_cPr (E F : {set A}) : Pr d F != 0 -> inde_events d E F -> `Pr_[E | F] = Pr d E.
proof: Proof. by move=> F0 EF; rewrite /cPr EF /Rdiv -mulRA mulRV ?mulR1. 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