proposition: Lemma cond_entropy1_RVE a : (`p_[% X, Y])`1 a != 0 -> cond_entropy1_RV a = cond_entropy1 `p_[% Y, X] a.
proof: Proof. move=> a0. rewrite /cond_entropy1_RV /cond_entropy1 /entropy; congr (- _). by apply: eq_bigr => b _; rewrite jfdist_condE// fdistX_RV2. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence