proposition: Lemma stopset_erasures_SP_BEC_stable p : SP_BEC0 BEC_y = iSP_BEC0 H y p -> stopset H (erasures (SP_BEC BEC_y)).
proof: Proof. move=> Hstable. have -> : erasures (SP_BEC BEC_y) = starFnext H y (iSP_BEC0 H y p.+1). rewrite (starFnext_iter_mxSumProd E Hc p.+1); congr erasures. rewrite /SP_BEC; congr (Esti H y _). by rewrite (SP_BEC0_is_a_fixpoint BEC_y) Hstable. apply: (fixed_point_stopset_starFnext Hc). by rewrite -Hstable SP_BEC0_is_a_fixpoint 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