proposition: Lemma Pr_domin_setXN (A B : finType) (P : {fdist A * B}) E F : Pr P (E `* F) != 0 -> Pr P`1 E != 0.
proof: Proof. by apply/contra => /eqP/Pr_domin_setX => ?; exact/eqP. 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