proposition: Lemma compatible : cancel_on code (Syslcode.encode dimlen CSM) (Syslcode.discard dimlen).
proof: Proof. move=> /= x; case/codewords' => ->. - rewrite (_ : Syslcode.discard _ _ = const_mx 1) ?encodeE //. rewrite /Syslcode.discard ffunE /Syslcode.DIS -trmx_const -trmx_mul. rewrite (@castmx_mulmx_cols_comm _ _ _ subnKC). by rewrite castmx_const -[in LHS]col_mx_const mul_row_col mul1mx mul0mx addr0 trmx_const. - rewrite (_ : Syslcode.discard _ _ = const_mx 0) ?encodeE //. by rewrite /Syslcode.discard ffunE /Syslcode.DIS mul0mx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code