proposition: Lemma mxSum_Star n0 m0 M : cols_starblank M s -> n0 \in s -> m0 \in 'F n0 -> mxSum H M m0 n0 = Star.
proof: Proof. move=> HB n0s m0n0. rewrite /mxSum mxE m0n0. set ls := rowVnextD1 _ _ _ _. rewrite /Sum. suff -> : has starblank ls by []. move/forallP : s_stopset => /(_ m0). case/(stopsetE_help n0s m0n0) => n2 [m0n2 [n0n2 n2s1]]. apply/hasP => /=; exists Star => //. apply/mapP; exists n2. by rewrite mem_enum in_setD1 eq_sym n0n2 -FnextE. by move/colP: (HB _ n2s1) => /(_ m0); rewrite !mxE m0n2. 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