proposition: Lemma stopset_erasures_SP_BEC : stopset H (erasures (SP_BEC BEC_y)).
proof: Proof. case: (SP_BEC0_is_iter BEC_y) => l Hstable. exact: (stopset_erasures_SP_BEC_stable Hstable). 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