proposition: Lemma size_idsA : size idsA = (n - m)%nat.
proof: Proof. move/card_uniqP: uniq_idsA <-. rewrite /idsA. suff: #|[set i : 'I_n | col i (Hamming.PCM m) \in non_unit_cols]| = (n - m)%nat. move <-. apply eq_card => i. by rewrite inE mem_filter mem_enum inE andbT. rewrite -card_non_unit -(card_imset _ col_PCM_inj). apply eq_card => c. have Hcols x : x \in non_unit_cols -> x \in [set col i (Hamming.PCM m) | i : 'I_n]. rewrite /non_unit_cols -cols_PCM !inE => ?; exact: ltnW. case Hc : (c \in non_unit_cols). apply/imsetP. case/imsetP: (Hcols _ Hc) => x Hx Hx'. by exists x => //; rewrite inE -Hx'. apply/negbTE. move/negbT: Hc; apply contra. case/imsetP => x Hx Hx'. by rewrite inE -Hx' in Hx. 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