proposition: Lemma all_starblank_colFNext_mxSum_stopset (stopset_s : stopset H s) M : cols_starblank H M s -> forall n0, n0 \in s -> all starblank (colFnext H (y ``_ n0) (col n0 (mxSum H M)) n0).
proof: Proof. move=> Hcols n0 n0s. apply/allP => /= l. rewrite in_cons. case/orP => [ /eqP -> | ]. move/subsetP : sy => /(_ _ n0s). by rewrite inE => /eqP ->. case/imageP => m1 m1n0. by rewrite mxE (mxSum_Star stopset_s Hcols n0s m1n0) => ->. 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