proposition: Lemma cinde_events_alt (E F G : {set A}) : cinde_events E F G <-> `Pr_d[ E | F :&: G] = `Pr_d[E | G] \/ Pr d (F :&: G) = 0.
proof: Proof. split=> [|[|FG0]]; rewrite /cinde_events. - rewrite product_rule_cond => H. have [/cPr_eq0 EG0|EG0] := eqVneq (`Pr_d[F | G]) 0. by rewrite /cPr EG0; right. by left; move/eqR_mul2r : H ; apply; apply/eqP. - by rewrite product_rule_cond => ->. - by rewrite /cPr -setIA setIC Pr_domin_setI // div0R FG0 div0R mulR0. 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