proposition: Lemma split_cons_tuples (Z : {set (sum_num_occ ta k.+1).-tuple B}) (Z' : {set ((sum_num_occ ta k).-tuple B) * N(enum_val k | ta).-tuple B}) : forall tb, tb \in Z -> split_tuple tb \in Z' -> tb \in cons_tuples @: Z'.
proof: Proof. case=> sb Hsb sb_Z sb_Z'. apply/imsetP. exists (split_tuple (Tuple Hsb)) => //. apply val_inj => /=. rewrite -{1}(cat_take_drop (sum_num_occ ta k) sb). f_equal. rewrite take_oversize // size_drop. clear -Hsb; move/eqP : Hsb => ->. by rewrite sum_num_occ_rec addKn. 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