proposition: Lemma Prod_colFNext_mxSum_stopset (stopset_s : stopset H s) M : cols_starblank H M s -> forall n0, n0 \in s -> Prod (colFnext H (y ``_ n0) (col n0 (mxSum H M)) n0) = Star.
proof: Proof. move=> ? ? ?; by apply/Prod_starblank_is_Star/all_starblank_colFNext_mxSum_stopset. 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