proposition: Lemma cols_1_inj : injective (fun i => col i 1 : 'cV['F_2]_m).
proof: Proof. move=> i j /= /matrixP/(_ j 0). rewrite !mxE eqxx /=. by case Hji : (j == i) => // _; apply/esym/eqP. 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