proposition: Lemma card_take_shell0 (k : 'I_#|A|) (Ha : N(enum_val k | ta) == 0) : #|take_shell ta V k.+1| <= #|take_shell ta V k|.
proof: Proof. move/eqP : (Ha). move/esym => Ha'. eapply leq_trans; first by apply (subset_leq_card_split_tuple (card_take_shell_incl0 Ha')). by rewrite cardsX cards1 muln1. 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