proposition: Lemma Pr_fdistA (A B C : finType) (P : {fdist A * B * C}) E F G : Pr (fdistA P) (E `* (F `* G)) = Pr P (E `* F `* G).
proof: Proof. rewrite /fdistA (@Pr_fdistmap _ _ (@prodA A B C))// ?imsetA//. exact: inj_prodA. 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