proposition: Lemma PiSP_BEC0_Star_inv l n0 m0 : n0 \in `V m0 -> (PiSP_BEC0 H y l) m0 n0 = Star -> y ``_ n0 = Star.
proof: Proof. case: l n0 m0 => [n0 m0 n0m0|]. rewrite /PiSP_BEC0 /= mxProd_mxStar_PCM_instance; last first. move=> n1; rewrite mxE; by case: ifPn. by rewrite PCM_instanceE // FnextE. move=> l n1 m0 n1m0. rewrite mxE FnextE n1m0. apply (@Prod_erase_Star _ _ H c E m0 n1 (iSP_BEC0 H y l.+1)). move=> j0; exact: (all_starletter_iSP_BEC0D1 l.+1 j0 m0). 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