proposition: Lemma all_starletter_iSP_BEC0D1 l n0 m0 : all [pred i | starletter ((col n0 (iSP_BEC0 H y l)) i ord0) (c ``_ n0)] (enum (`F n0 :\ m0)).
proof: Proof. apply/allP => /= m1. rewrite mem_enum in_setD1 => /andP[m1m0 m1Fn0]. by move/allP: (all_starletter_iSP_BEC0 Hc E l n0) => /(_ m1); rewrite mem_enum => /(_ m1Fn0). 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