proposition: Lemma product_rule (E F : {set A}) : Pr d (E :&: F) = `Pr_[E | F] * Pr d F.
proof: Proof. rewrite /cPr; have [PF0|PF0] := eqVneq (Pr d F) 0. by rewrite setIC (Pr_domin_setI E PF0) div0R mul0R. by rewrite -mulRA mulVR ?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