proposition: Lemma Pr_DMC_out m (S : {set 'rV_m}) : Pr ((P `X W) `^ m) [set x | (rV_prod x).2 \notin S] = Pr (`O(P , W) `^ m) (~: S).
proof: Proof. rewrite {1}/Pr big_rV_prod /= -(pair_big_snd _ _ [pred x | x \notin S]) //=; last first. move=> tab /=. rewrite SetDef.pred_of_setE /= SetDef.finsetE /= ffunE. do 2 f_equal. by apply/rowP => a; rewrite !mxE. rewrite /= /Pr /= exchange_big /=; apply: eq_big => tb; first by rewrite !inE. move=> Htb. rewrite fdist_rVE. under [RHS]eq_bigr do rewrite fdist_outE. rewrite bigA_distr_bigA /=. rewrite (reindex_onto (fun p : 'rV[A]_m => [ffun x => p ord0 x]) (fun y : {ffun 'I_m -> A} => \row_(i < m) y i)) /=; last first. by move=> f _; apply/ffunP => /= m0; rewrite ffunE mxE. apply: eq_big => ta. by rewrite inE; apply/esym/eqP/rowP => a; rewrite mxE ffunE. move=> Hta. rewrite fdist_rVE /=; apply eq_bigr => l _. by rewrite fdist_prodE -fst_tnth_prod_rV -snd_tnth_prod_rV ffunE -RmultE mulRC. 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