proposition: Lemma fdistX_prod2 {R: realType} (A B : finType) (P : fdist R A) (W : A -> fdist R B) : (fdistX (P `X W))`2 = P.
proof: Proof. by rewrite fdistX2 fdist_prod1. 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