proposition: Lemma typed_tuples_not_empty : { t | t \in T_{P} }.
proof: Proof. apply sigW. case: typed_tuples_not_empty' => x [Hx H]. by exists (Tuple Hx). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq