proposition: Lemma len_dim : n = (2 ^ m).-1.
proof: Proof. rewrite /n /len !expnS -subn1 doubleB -muln2 -subSn; last first. by rewrite -muln2 mulnC -mulnA leq_mul2l /= -expnSr expn_gt0. by rewrite -muln2 mul1n subn2 /= mulnC. 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