proposition: Lemma const_mx_in_code b : const_mx b \in code.
proof: Proof. rewrite /code -(encodeE b dimlen); exact: Syslcode.encode_code. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code