proposition: Lemma cols_1 : [set c : 'cV['F_2]_m | wH c^T == 1%nat] = [set col i 1 | i : 'I_m].
proof: Proof. apply/setP => /= i. rewrite in_set; apply/esym. case HwH : (wH i^T == _). apply/imsetP. move: HwH. rewrite wH_num_occ num_occ.num_occ_alt => /cards1P[x Hx]. exists x => //. apply/colP => j. rewrite !mxE /=. move/setP/(_ j): Hx. rewrite in_set1 in_set tnth_mktuple mxE => <-. by rewrite F2_eq1; case: F2P. apply/negbTE; move/negbT: HwH; apply contra. case/imsetP => x Hx ->. by apply/eqP/wH_col_1. 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