proposition: Theorem v_scode_direct : exists n : nat, exists f : encT X (seq bool) n, injective f /\ @E_leng_cw _ _ P f / n%:R < `H P + epsilon.
proof: Proof. apply: (ex_intro _ (n0.+1)). have: (n0 < n0.+1)%nat by[]. case/v_scode'=> // sc [fphi ccl]. apply: (ex_intro _ (enc sc)). by split => //; exact: (can_inj fphi). 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