proposition: Lemma card_take_shell_incl0 (k : 'I_#|A|) (Ha : 0 = N(enum_val k | ta)) tb : tb \in take_shell ta V k.+1 -> split_tuple tb \in setX (take_shell ta V k) (set1 (tcast Ha [tuple of ([::] : seq B)])).
proof: Proof. move=> tbV. destruct tb as [s Hs]. move: tbV; rewrite /take_shell [in X in X -> _]/= => /imsetP[tb' tb'V]. move/esym/tcast2tval; rewrite [X in X -> _]/= => tb's. rewrite /split_tuple /= in_setX; apply/andP; split. - apply/imsetP; exists tb' => //. apply/val_inj => /=. rewrite eq_tcast /=. by rewrite -tb's sum_num_occ_rec take_takel// leq_addr. - rewrite in_set. apply/eqP/val_inj => /=. by rewrite eq_tcast -Ha take0. 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