fact: Definition approx (c : 'rV['F_2]_n) (M : 'M[letter]_(m, n)) := [forall i, map_mx Bit c <=m map_mx blank_to_star (row i M)].
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode