proposition: Lemma card_non_unit : #|non_unit_cols| = (n - m)%nat.
proof: Proof. apply/eqP. rewrite -(eqn_add2r #|unit_cols|). apply/eqP. have: #|non_unit_cols :&: unit_cols| = #|(set0 : {set 'cV['F_2]_m})|. apply eq_card=> c. rewrite !in_set andbC. apply/negP. by case/andP => /eqP ->. rewrite cards0 => Hint. rewrite -(subn0 (_ + _)%nat) -[X in (_ + _ - X)%nat]Hint. by rewrite -cardsU card_unit_cols (subnK (Hamming.dim_len m')) card_all_cols. 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