proposition: Lemma fdistX_prod_out (W : `Ch(A, B)) (P : {fdist A}) : (fdistX (P `X W))`1 = `O(P, W).
proof: Proof. rewrite fdistX1; apply/fdist_ext => b; rewrite fdist_outE fdist_sndE. by under eq_bigr do rewrite fdist_prodE -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