proposition: Lemma has_starblank_rowVnextD1 (A B : 'M_(m, n)) y m0 n0 : mxProd y A <=m mxProd y B -> has starblank (rowVnextD1 (row m0 (mxProd y A)) m0 n0) -> has starblank (rowVnextD1 (row m0 (mxProd y B)) m0 n0).
proof: Proof. move=> AB /hasP[l l_row Hl]; move: l_row => /mapP[n1 Hn1 ln1]. apply/hasP => /=; exists l => //. apply/mapP; exists n1 => //. move/'forall_forallP/(_ m0 n1) : AB. move: Hl. rewrite {}ln1 {l} // mxE [(row _ _) _ _]mxE. move/starblankP => /orP[/eqP ->|/eqP ->]; by [move/lel_Star | move/lel_Blank]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode