fact: Definition no_failure := [set x : 'rV[A]_k.+1 | dec sc (enc sc x) == x].
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code