proposition: Lemma fdistX_prod : fdistX (Q `x P) = P `x Q.
proof: Proof. by apply/fdist_ext => -[a b]; rewrite fdistXE !fdist_prodE mulrC. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext