proposition: Lemma not_erasure_SP_BEC n0 : n0 \notin E -> (SP_BEC (ex_intro _ c (BEC_IO_erase E Hc))) ``_ n0 = Bit (c ``_ n0).
proof: Proof. move=> n0E. rewrite /SP_BEC. case: (SP_BEC0_is_iter (ex_intro _ c (BEC_IO_erase E Hc))) => l ->. rewrite /Esti mxE /colFnext mxE (negbTE n0E) Prod_cons_starletter //. exact: all_starletter_iSP_BEC0. 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