proposition: Lemma largest_stopset_erasures_SP_BEC : largest_stopset H E = erasures (SP_BEC BEC_y).
proof: Proof. rewrite -(@largest_stopset_is_unique _ _ H _ (erasures (SP_BEC BEC_y))) //. split; first by apply erasures_SP_BEC_subset. split; first by apply all_stopsets_in_erasures_in_SP_BEC. exact: stopset_erasures_SP_BEC. 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