proposition: Lemma drop_take_is_filter_zip (tb : n.-tuple B): drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) (zip ta tb)) = filter (fun p => p.1 == enum_val k) (zip ta tb).
proof: Proof. set a := enum_val k. case/card_gt0P : Bnot0 => b _. rewrite -(mkseq_nth (a, b) (zip ta tb)) -map_take -map_drop filter_map size_zip 2!size_tuple minnn. f_equal. rewrite drop_take_iota; last by rewrite sum_num_occ_inc_loc sum_num_occ_leq_n. apply eq_in_filter => /= i. rewrite mem_iota leq0n add0n /= => Hi. rewrite nth_zip /=; last by rewrite 2!size_tuple. transitivity (ta!_(Ordinal Hi) == a); by [rewrite -sum_num_occ_is_enum_val | rewrite (tnth_nth a)]. 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