proposition: Lemma Pr_DMC_fst (Q : 'rV_n -> bool) : Pr ((P `X W) `^ n) [set x | Q (rV_prod x).1 ] = Pr P `^ n [set x | Q x].
proof: Proof. rewrite {1}/Pr big_rV_prod /= -(pair_big_fst _ _ [pred x | Q x]) //=; last first. move=> t /=. rewrite SetDef.pred_of_setE /= SetDef.finsetE /= ffunE. congr (Q _). by apply/rowP => a; rewrite !mxE. transitivity (\sum_(i | Q i) P `^ n i * (\sum_(y in 'rV[B]_n) W ``(y | i))). apply: eq_bigr => ta Sta; rewrite big_distrr; apply: eq_bigr => tb _ /=. rewrite DMCE [in RHS]fdist_rVE -[in RHS]big_split /= fdist_rVE. by apply eq_bigr => j _; rewrite fdist_prodE /= -fst_tnth_prod_rV -snd_tnth_prod_rV. transitivity (\sum_(i | Q i) P `^ _ i). by apply eq_bigr => i _; rewrite (FDist.f1 (W ``(| i))) mulR1. by rewrite /Pr; apply eq_bigl => t; rewrite !inE. 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