proposition: Lemma submx_in_gen_eq m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) : (V *m A <= V -> (in_gen U <= in_gen V) = (U <= V))%MS.
proof: Proof. move=> sVA_V; apply/idP/idP=> siUV; last exact: submx_in_gen. apply/row_subP=> i; rewrite -[row i U]in_genK in_gen_row. case/submxP: (row_subP siUV i) => u ->{i U siUV}. rewrite mulmx_sum_row val_gen_sum summx_sub // => j _. rewrite val_genZ val_gen_row in_genK rowE -mulmxA mulmx_sub //. rewrite [mxval _]horner_poly mulmx_sumr summx_sub // => [[k _]] _ /=. rewrite mulmxA mul_mx_scalar -scalemxAl scalemx_sub {u j}//. elim: k => [|k IHk]; first by rewrite mulmx1. by rewrite exprSr mulmxA (submx_trans (submxMr A IHk)). 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)