proposition: Lemma Pr_fdistC12 (A B C : finType) (P : {fdist A * B * C}) E F G : Pr (fdistC12 P) (E `* F `* G) = Pr P (F `* E `* G).
proof: Proof. rewrite /Pr !big_setX /= exchange_big; apply eq_bigr => a aF. by apply eq_bigr => b bE; apply eq_bigr => c cG; rewrite fdistC12E. 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