proposition: Lemma DMCE (A B : finType) n (W : `Ch(A, B)) b a : W ``(b | a) = \prod_(i < n) W (a ``_ i) (b ``_ i).
proof: Proof. by rewrite /DMC.c; unlock; rewrite ffunE. 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