proposition: Lemma encodeE (b : 'F_2) H : Syslcode.encode H CSM (const_mx b) = const_mx b.
proof: Proof. rewrite /row_of_tuple /Syslcode.encode /Syslcode.GEN ffunE. rewrite (mulmx_castmx_cols_comm subnKC); apply/rowP => i. rewrite mxE castmxE /= cast_ord_id mul_mx_row mulmx1 mxE. case: splitP => [j _| k /= bk]; first by rewrite mxE. rewrite mxE (bigD1 ord0) //= !mxE oppr_char2 // mulr1 big_pred0 ?addr0 //. by move=> x /=; rewrite (ord1 x) eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code