proposition: Lemma Pr_DMC_rV_prod (Q : 'rV_n * 'rV_n -> bool) : Pr (((P `^ n) `X (W ``^ n))) [set x | Q x] = Pr ((P `X W) `^ n) [set x | Q (rV_prod x)].
proof: Proof. rewrite /Pr [RHS]big_rV_prod /=; apply: eq_big => y. by rewrite !inE prod_rVK. rewrite inE => Qy; rewrite fdist_prodE DMCE fdist_rVE -big_split /= fdist_rVE. apply: eq_bigr => i /= _. by rewrite fdist_prodE -snd_tnth_prod_rV -fst_tnth_prod_rV. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond