proposition: Lemma erasures_erase y E : erasures (erase y E) = E.
proof: Proof. apply/setP => /= n0; by rewrite !inE !mxE; case: ifPn. Qed.
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