proposition: Lemma num_occ_num_co_occ (b : B) (sb : seq B) (tb : n.-tuple B) : sb = drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) tb) -> N(b | sb) = N(enum_val k, b | ta, tb).
proof: Proof. move=> Hsb. set a := enum_val k. rewrite /num_co_occ /num_occ // Hsb -!size_filter. rewrite -(_ : filter (fun p => p.2 == b) (filter (fun p => p.1 == a) (zip ta tb)) = filter (pred1 (a, b)) (zip ta tb)) ; last first. rewrite -filter_predI /predI; apply eq_in_filter => i Hi /=. symmetry; by rewrite andbC {1}(surjective_pairing i) xpair_eqE. set l1 := drop _ _. set l2 := filter _ (zip ta tb). suff -> : l1 = unzip2 l2 by rewrite filter_map size_map. by rewrite /l1 /l2 {l1 l2} drop_take_is_unzip2_filter. 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