fact: Definition jtyp_seq (t : 'rV[A * B]_n) := [&& typ_seq P epsilon (rV_prod t).1, typ_seq (`O(P , W)) epsilon (rV_prod t).2 & typ_seq ((P `X W)) epsilon t].
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