proposition: Lemma col_PCM_inj : injective (fun i => col i (Hamming.PCM m)).
proof: Proof. move=> i j Hij. rewrite 2!col_matrix in Hij. have Hi := Hamming.len_two_m i. have Hj := Hamming.len_two_m j. rewrite -(Pnat.Nat2Pos.id i.+1) // in Hij Hi. rewrite -(Pnat.Nat2Pos.id j.+1) // in Hij Hj. rewrite !BinPos_nat_of_P_nat_of_pos in Hij Hi Hj. move/trmx_inj in Hij. have Hpos := nat_of_pos_inj (rV_of_nat_inj Hi Hj Hij). have Hij' : i.+1 = j.+1 by apply Pnat.Nat2Pos.inj. apply/eqP. rewrite -(addn1 i) -(addn1 j) in Hij'. move/eqP: Hij'. by rewrite eqn_add2r. 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