proposition: Lemma erasures_SP_BEC_subset : erasures (SP_BEC (ex_intro _ c (BEC_IO_erase E Hc))) \subset E.
proof: Proof. apply/subsetP => /= n0. rewrite /erasures inE /SP_BEC. case/boolP: (n0 \in E) => [//|n0E]. by rewrite not_erasure_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