proposition: Lemma submx_in_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) : (U <= V -> in_gen U <= in_gen V)%MS.
proof: Proof. move=> sUV; apply/row_subP=> i; rewrite -in_gen_row. case/submxP: (row_subP sUV i) => u ->{i}. rewrite mulmx_sum_row in_gen_sum summx_sub // => j _. by rewrite in_genZ in_gen_row scalemx_sub ?row_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)