proposition: Lemma shell_not_empty_sorted : exists tb, tb \in V.-shell ta.
proof: Proof. case: (shell_not_empty') => tb [Htb H]; by exists (Tuple Htb). 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