proposition: Lemma drop_take_is_unzip2_filter (tb : n.-tuple B) : drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) tb) = unzip2 (filter (fun ab => ab.1 == enum_val k) (zip ta tb)).
proof: Proof. transitivity (unzip2 (drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) (zip ta tb)))). by rewrite /unzip2 map_drop map_take -/(unzip2 (zip ta tb)) unzip2_zip // 2!size_tuple. by rewrite drop_take_is_filter_zip. 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