proposition: Lemma set_typ_seq_not0 : aep_bound P epsilon <= n.+1%:R -> #| `TS P n.+1 epsilon | <> O.
proof: Proof. move/Pr_TS_1 => H. case/boolP : (#| `TS P n.+1 epsilon | == O) => [|Heq]; last by apply/eqP. rewrite cards_eq0 => /eqP Heq. rewrite Heq Pr_set0 in H. lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep