fact: Definition letter_unpickle (n : nat) := match n with | O => Some (Bit 0) | 1 => Some (Bit 1) | 2 => Some Star | 3 => Some Blank | _ => None end.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode