proposition: Lemma card_take_shell_incl (k : 'I_#|A|) (Ha : N(enum_val k | ta) != 0 ) tb : tb \in take_shell ta V k.+1 -> split_tuple tb \in setX (take_shell ta V k) (T_{type_of_row Ha}).
proof: Proof. move=> Hlhs. destruct tb as [sb Hsb]. rewrite /take_shell /= in Hlhs. move:Hlhs. case/imsetP => tb Htb_1 Htb_2. symmetry in Htb_2; move/tcast2tval in Htb_2; rewrite /= in Htb_2. rewrite /split_tuple /= in_setX. apply/andP; split. - apply/imsetP; exists tb => //; apply/val_inj => /=. by rewrite eq_tcast /= -Htb_2 sum_num_occ_rec take_takel // leq_addr. - rewrite in_set. set t := Tuple _. have Ht : tval t = take N(enum_val k | ta) (drop (sum_num_occ ta k) sb) by []. apply/forallP => b. rewrite /= ffunE /=. move: Htb_1. rewrite in_set ffunE. move/forallP/(_ (enum_val k))/forallP/(_ b)/eqP => /= H. rewrite -{1}H. rewrite -Htb_2 in Ht. apply/eqP. have Ht2 : tval t = drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) tb). rewrite Ht {1}sum_num_occ_rec take_drop take_takel; last by rewrite addnC. by rewrite addnC sum_num_occ_rec. congr (_ %:R / _%:R)%R. exact/esym/num_occ_num_co_occ. 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