proposition: Lemma TS_0_is_typ_seq (k_k0 : aep_bound P epsilon <= n.+1%:R) : TS_0 k_k0 \in `TS P n.+1 epsilon.
proof: Proof. rewrite /TS_0. apply/enum_valP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep