proposition: Lemma fdist_condE a : fdist_cond E0 a = `Pr_P [[set a] | E].
proof: Proof. by rewrite /fdist_cond; unlock; rewrite ffunE. 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