fact: Definition eql (a b : letter) := match a, b with | Bit a', Bit b' => a' == b' | Star, Star => true | Blank, Blank => true | _, _ => false end.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode