proposition: Lemma letterP l : letter_spec l (l == Bit 0) (l == Bit 1) (l == Blank) (l == Star).
proof: Proof. case: l; [|by constructor|by constructor]. case/F2P; by constructor. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode