proposition: Lemma output_type_out_entropy : `H (`tO( V )) = `H(P `o V).
proof: Proof. rewrite /entropy; f_equal. apply eq_bigr => b _; by rewrite output_type_out_fdist. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types