proposition: Lemma card_shelled_tuples_leq_prod_card : #| V.-shell ta | <= \prod_ ( i < #|A|) card_type_of_row i.
proof: Proof. rewrite -full_take_shell [X in _ <= X](_ : _ = \prod_(i < #|A| | i < #|A|) card_type_of_row i); last first. apply eq_bigl => ?; symmetry; by apply ltn_ord. exact (split_nocc_rec (leqnn #|A|)). 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