proposition: Lemma sum_num_occ_size : forall (a : (sum_num_occ ta k.+1).-tuple B), sum_num_occ ta k <= size a.
proof: Proof. case=> a. rewrite sum_num_occ_rec /= => /eqP ->. by rewrite -{1}(addn0 (sum_num_occ ta k)) leq_add2l. 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