proposition: Lemma full_take_shell : #| take_shell #|A| | = #| V.-shell ta |.
proof: Proof. apply card_imset; rewrite /injective => /= v v' vv'. exact: (tcast_take_inj (full_sum_num_occ_n ta (leqnn #|A|)) vv'). 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