proposition: Lemma card_all_cols : #|non_unit_cols :|: unit_cols| = n.
proof: Proof. rewrite /non_unit_cols /unit_cols. transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|. apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt. by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj. 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