proposition: Lemma cond_entropy1_fdistAC b c : cond_entropy1 (fdistA PQR) (b, c) = cond_entropy1 (fdistA (fdistAC PQR)) (c, b).
proof: Proof. rewrite /cond_entropy1; congr (- _). by apply eq_bigr => a _; rewrite -!setX1 jcPr_fdistA_AC. 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