fact: Definition set_jtyp_seq : {set 'rV[A * B]_n} := [set tab | jtyp_seq tab].
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext logb ssralg_ext bigop_ext fdist proba entropy aep typ_seq channel