proposition: Lemma PiSP_BEC0_Star_inv_stable l n0 m0 : n0 \in `V m0 -> (PiSP_BEC0 H y l) m0 n0 = Star -> iSP_BEC0 H y l = iSP_BEC0 H y l.+1 -> forall n1, n1 \in `V m0 -> n1 != n0 -> (iSP_BEC0 H y l) m0 n1 = Star.
proof: Proof. move=> m0n0 H1 Hstable n1 n1m0 n1n0. rewrite Hstable mxE FnextE n1m0. rewrite /Sum ifT //. apply/hasP => //=; exists Star => //. apply/mapP; exists n0 => //. by rewrite mem_enum in_setD1 eq_sym n1n0. by rewrite mxE. 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