proposition: Lemma BEC_IO_erase m (H : 'M['F_2]_(m, n)) c E : syndrome H c = 0 -> c BEC( H ) (erase c E).
proof: Proof. move=> ?; rewrite /BEC_IO; split => //; exact: lel_mat_erase. 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