proposition: Lemma iSP_BEC0_star_inv l m0 n0 : (iSP_BEC0 H y l.+1) m0 n0 = Star -> exists n1, n1 != n0 /\ m0 \in `F n1 /\ (PiSP_BEC0 H y l) m0 n1 = Star.
proof: Proof. rewrite mxE. case: ifPn => m0n0. rewrite /Sum. case: ifP; last by []. case/hasP => /= ln1. case/mapP => n1 Hn1 Hln1 Kln1 _. exists n1 => //. move: Hn1. rewrite mem_enum in_setD1 => /andP[-> n1m0]; split => //. rewrite FnextE n1m0; split => //. move: (@starletter_PiSP_BEC0 l n1 m0). rewrite FnextE => /(_ n1m0). rewrite /starletter => /orP[/eqP //| /eqP abs]. exfalso. move: Kln1. by rewrite Hln1 mxE abs. case: l => [|l]. by rewrite /= !mxE (negbTE m0n0). move: (iSP_BEC0_Blank y l m0n0). by rewrite !mxE (negbTE m0n0) /= => ->. 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