proposition: Lemma all_starletter_iSP_BEC0 : forall l n0, all [pred i | starletter ((col n0 (iSP_BEC0 H (erase c E) l)) i ord0) (c ``_ n0)] (enum ('F n0)).
proof: Proof. case => [n0 /=|]. apply/allP => m1 m1n0 /=. move/allP: (all_mxStar H n0) => /(_ _ m1n0) /=. by rewrite /= 3!mxE => /eqP ->. exact: all_starletter_iSP_BEC0S. 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