proposition: Lemma Pr_fdist_cond G : Pr (fdist_cond E0) G = `Pr_P [ G | E ].
proof: Proof. rewrite /Pr; under eq_bigr do rewrite fdist_condE. rewrite -big_distrl /=; congr (_ / _). rewrite (_ : _ :&: _ = \bigcup_(i in G) ([set i] :&: E)); last first. by rewrite -big_distrl /= -bigcup_set1. rewrite [in RHS]/Pr big_bigcup_partition // => i j ij. rewrite -setI_eq0; apply/eqP/setP => a; rewrite !inE. apply/negbTE; rewrite !negb_and. have [->/=|//] := eqVneq a i. by rewrite ij /= orbT. 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