proposition: Lemma len_two_m (i : 'I_n) : i.+1 < 2 ^ m.
proof: Proof. by rewrite (leq_ltn_trans (ltn_ord i)) // len_dim -ltnS prednK // expn_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel