proposition: Lemma all_stopsets_in_erasures_in_SP_BEC c E (Hc : syndrome H c = 0) : covered_by (stopset H) E (erasures (SP_BEC (ex_intro _ c (BEC_IO_erase E Hc)))).
proof: Proof. apply/forallP => /= s; apply/implyP. rewrite inE => /andP[H0 H1]. apply stopset_subset_erasures_SP_BEC => //; by rewrite erasures_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