proposition: Lemma PiSP_BEC0S_Star_inv l n0 m0 : n0 \in `V m0 -> (PiSP_BEC0 H y l.+1) m0 n0 = Star -> forall m1, m1 \in `F n0 :\ m0 -> (iSP_BEC0 H y l.+1) m1 n0 = Star.
proof: Proof. move=> n0m0 H1 m1 m1n. rewrite mxE FnextE n0m0 in H1. have : (forall n1, all [pred i | starletter ((col n1 (mxSum H (PiSP_BEC0 H y l))) i ord0) (c ``_ n1)] (enum (`F n1 :\ m0))). move=> n2; apply/allP => m2 m2n2. move: (all_starletter_iSP_BEC0 Hc E l.+1). move/(_ n2) => /allP/(_ m2). by move: m2n2; rewrite 2!mem_enum in_setD1 => /andP[m2m0 m2Fn2] /(_ m2Fn2). move/(@Prod_erase_Star _ _ H c E m0 n0 (mxSum H (PiSP_BEC0 H y l))). move/(_ H1) => [H2 H3]. by apply H2. 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