proposition: Lemma dec_enc m : phi (f m) = Some m.
proof: Proof. rewrite /= !ffunE /= /hamming_repair. move: (hamming_err_enc m); rewrite !ffunE /= => ->. rewrite addr0 /Hamming'.discard -mulmxA. suff -> : Hamming'.GEN r' *m (Hamming'.mx_discard r')^T = 1%:M by rewrite mulmx1. apply trmx_inj; by rewrite trmx1 trmx_mul trmxK Hamming'.mx_discard_GEN. 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