proposition: Lemma starletter_PiSP_BEC0 : forall l n0 m0, m0 \in `F n0 -> starletter ((PiSP_BEC0 H y l) m0 n0) (c ``_ n0).
proof: Proof. case => [ | l] n0 m0 n0m0. rewrite /PiSP_BEC0 mxProd_mxStar_PCM_instance; last first. move=> n1; rewrite mxE; by case: ifPn. rewrite PCM_instanceE // mxE. case: ifPn => // _; by rewrite /starletter eqxx orbC. exact: (starletter_mxProd_erase E n0m0 (all_starletter_iSP_BEC0S Hc _ _ _)). 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