proposition: Lemma drop_take_is_filter : drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) ta) = filter (pred1 (enum_val k)) ta.
proof: Proof. apply (@eq_from_nth _ (enum_val k)) => [|i Hi]. rewrite size_drop size_take size_tuple -/(minn (sum_num_occ ta k.+1) n) minn_sum_num_occ_n. by rewrite (sum_num_occ_sub _ k) /num_occ -size_filter. rewrite size_drop size_take size_tuple -/(minn (sum_num_occ ta k.+1) n) minn_sum_num_occ_n ltn_subRL in Hi. rewrite nth_drop nth_take => //. have Hsumk : sum_num_occ ta k + i < n by apply (leq_trans Hi (sum_num_occ_leq_n ta k.+1)). transitivity (enum_val k). transitivity (ta!_(Ordinal Hsumk)). by rewrite [in X in _ = X](tnth_nth (enum_val k)). apply sum_num_occ_enum_val => //=; by rewrite Hi andbT leq_addr. rewrite -ltn_subRL (sum_num_occ_sub ta k) in Hi. by rewrite filter_pred1_num_occ nth_nseq Hi. 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