proposition: Lemma split_nocc_rec : forall k, k <= #|A| -> #|take_shell ta V k| <= \prod_ (i < #|A| | i < k) card_type_of_row i.
proof: Proof. elim. - move=> _; rewrite big_pred0; last by move=> ? /=; rewrite ltn0. rewrite -(expn0 #|B|) -[X in _ <= expn _ X](sum_num_occ_0 ta) -card_tuple -cardsT. by apply subset_leq_card, subsetT. - move=> k IH HSk /=. move: (IH (ltnW HSk)) => {}IH. rewrite (bigD1 (Ordinal HSk)) //=. rewrite (eq_bigl (fun i : 'I_#|A| => i < k) _); last first. move=> i /=. case/boolP : (i < k) => Hcase. - have -> : i != Ordinal HSk by rewrite neq_ltn; apply/orP; apply or_introl. by rewrite andbC /= ltnW. - rewrite andbC -ltn_neqAle. by move/negbTE : Hcase => ->. rewrite /card_type_of_row; case: Bool.bool_dec => [e|/Bool.eq_true_not_negb e]. rewrite mul1n. eapply leq_trans; [exact: (card_take_shell0 e) | by []]. apply (leq_trans (card_take_shell e)). rewrite mulnC leq_pmul2l //. apply/card_gt0P. set Q := type_of_row e. case: (typed_tuples_not_empty_alt e Q) => tb Htb. by exists tb. 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