proposition: Lemma all_starblank_colFNextD1_mxSum_stopset (stopset_s : stopset H s) M : cols_starblank H M s -> forall n0, n0 \in s -> forall m0, all starblank (colFnextD1 H (y ``_ n0) (col n0 (mxSum H M)) n0 m0).
proof: Proof. move=> Hcols n0 n0s m0. move/allP: (all_starblank_colFNext_mxSum_stopset stopset_s Hcols n0s) => H0. apply/allP => l; rewrite inE => /orP[|] H1. move: (H0 l); rewrite inE H1 orTb; by apply. move: (H0 l); rewrite inE; apply; apply/orP; right. case/mapP : H1 => x Hx Hl. apply/mapP; exists x => //. by move: Hx; rewrite !mem_enum in_setD1 => /andP[]. 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