proposition: Lemma cond_entropy_chanE : `H(W | P) = cond_entropy (fdistX (P `X W)).
proof: Proof. rewrite /cond_entropy_chan. have := chain_rule (P `X W); rewrite /joint_entropy => ->. by rewrite fdist_prod1 addRC addRK. 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