fact: Definition enc_typ x := let i := seq.index x (enum (`TS P n epsilon)) in Tuple (size_bitseq_of_nat i (Z.abs_nat L_typ)).
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