proposition: Lemma codewords : [set cw in code] = [set const_mx 1 ; 0]%R.
proof: Proof. apply/setP => x; apply/idP/idP. - by rewrite inE => /codewords' -[|] ->; rewrite !inE !eqxx // orbT. - by rewrite !inE => /orP[|] /eqP ->; rewrite const_mx_in_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