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