fact: Definition erasures (y : 'rV[letter]_n) : {set 'I_n} := [set i | y ``_ i == Star].
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) f2 ssr_ext ssralg_ext max_subset num_occ hamming ldpc_erasure tanner linearcode