proposition: Lemma card_le_TS_Lt : INR #| `TS P n epsilon | <= INR #|[ set : (Z.abs_nat L_typ).-tuple bool]|.
proof: Proof. apply: (Rle_trans _ _ _ (TS_sup _ _ _)). rewrite cardsT /= card_tuple /= card_bool. rewrite -natRexp2. apply: Exp_le_increasing => //. rewrite INR_Zabs_nat. - exact: (proj1 (ceilP _)). - by apply: le_IZR; apply: ltRW; apply: Lt_pos. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code