proposition: Lemma cols_PCM : [set c | wH c^T >= 1] = [set col i (Hamming.PCM m) | i : 'I_n].
proof: Proof. apply/setP => i. rewrite in_set. case Hi : (0 < wH i^T). apply/esym/imsetP. have H0 : nat_of_rV i^T - 1 < n. have iup := nat_of_rV_up i^T. rewrite /n Hamming.len_dim -subn1 ltn_sub2r //. by rewrite -{1}(expn0 2) ltn_exp2l // ltnW. exists (Ordinal H0) => //. apply/trmx_inj. rewrite col_matrix /= trmxK -{1}(nat_of_rVK i^T) subn1 prednK // lt0n nat_of_rV_eq0. by apply/eqP => abs; rewrite abs lt0n wH0 eqxx in Hi. apply/esym/negbTE; move/negbT : Hi; apply contra. case/imsetP => j Hj ->. case HwH : (wH (col j (Hamming.PCM m))^T); last by []. exfalso. move/eqP: HwH. rewrite col_matrix wH_eq0 trmxK => /eqP. by apply rV_of_nat_neq0 => //; apply Hamming.len_two_m. 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