proposition: Lemma stopset_subset_erasures_SP_BEC (stopset_s : stopset H s) : s \subset erasures (SP_BEC BEC_y).
proof: Proof. rewrite /SP_BEC. case: (SP_BEC0_is_iter BEC_y) => x ->. apply/subsetP => /= n0 n0_in_s. rewrite /erasures inE /SP_BEC. move Halpha : (mxStar H) => alpha. move: (subset_erasures_Esti). rewrite Halpha. move/subsetP => /(_ _ n0_in_s) => Hn0. rewrite !inE /SP_BEC /= in Hn0. move: cols_starblank_mxProd. rewrite /iSP_BEC0. rewrite {}Halpha => Hbeta. move: x alpha Hbeta Hn0. elim => [ //= | lmax IHmax ] alpha Hbeta. rewrite -(addn1 lmax) iterD => EstiStar . apply IHmax. rewrite /= /cols_starblank => n1 Hns1; apply/colP => m1. rewrite !mxE. case: ifPn => /= m1n1. by apply: Prod_colFNextD1_mxSum_stopset. rewrite (negbTE m1n1). by move: (Hbeta _ Hns1) => /colP/(_ m1); rewrite !mxE (negbTE m1n1). rewrite mxE. exact/eqP/Prod_colFNext_mxSum_stopset. 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