proposition: Lemma entropy_H2 (card_A : #|A| = 2%nat) (p : {prob R}) : H2 (Prob.p p) = entropy (fdist_binary card_A p (Set2.a card_A)).
proof: Proof. rewrite /H2 /entropy Set2sumE /= fdist_binaryxx !fdist_binaryE. by rewrite eq_sym (negbTE (Set2.a_neq_b _)) oppRD addRC. 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