proposition: Lemma fdist_prodK : cancel fdist_split (uncurry (@fdist_prod _ A B)).
proof: Proof. move=> PQ; apply/fdist_ext => ab; rewrite fdist_prodE. have [Ha|Ha] := eqVneq (PQ`1 ab.1) 0. rewrite Ha GRing.mul0r; apply/esym/(dominatesE (Prod_dominates_Joint PQ)). by rewrite fdist_prodE Ha GRing.mul0r. rewrite jfdist_condE // -fdistX2 GRing.mulrC. rewrite -(Pr_set1 _ ab.1) -RmultE -jproduct_rule setX1 Pr_set1 fdistXE. by case ab. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba