proposition: Lemma card_take_shell (k : 'I_#|A|) (Ha : N(enum_val k | ta) != 0) : #|take_shell ta V k.+1| <= #|take_shell ta V k| * #| T_{type_of_row Ha} |.
proof: Proof. rewrite -cardX -[X in _ <= X]cardsE. apply (subset_leq_card_split_tuple (card_take_shell_incl Ha)). 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