proposition: Lemma subset_leq_card_split_tuple (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') -> #|Z| <= #|Z'|.
proof: Proof. move=> Hincl. have <- : #| cons_tuples @: Z' | = #|Z'|. apply: card_in_imset; case=> [a1 a2] [b1 b2] Ha Hb [] /eqP. rewrite eqseq_cat; last by rewrite 2!size_tuple. case/andP => /eqP H1 /eqP H2. f_equal; by apply val_inj. apply/subset_leq_card/subsetP => tb Htb. by apply (split_cons_tuples Htb), Hincl. 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