proposition: Lemma encode_inj : injective (enc channel_code).
proof: Proof. move=> /= i j; rewrite !ffunE => /(congr1 (fun t => mx_discard *m t^T)). by rewrite !trmx_mul !mulmxA mx_discard_GEN !mul1mx => /trmx_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