proposition: Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) : (U <= rowval_gen V)%MS = (in_gen U <= V)%MS.
proof: Proof. rewrite genmxE; apply/idP/idP=> sUV. apply: submx_trans (submx_in_gen sUV) _. apply/row_subP; case/mxvec_indexP=> i k; rewrite -in_gen_row rowK mxvecE mxE. rewrite -mxval_grootXn -val_gen_row -val_genZ val_genK scalemx_sub //. exact: row_sub. rewrite -[U]in_genK; case/submxP: sUV => u ->{U}. apply/row_subP=> i0; rewrite -val_gen_row row_mul; move: {i0 u}(row _ u) => u. rewrite mulmx_sum_row val_gen_sum summx_sub // => i _. rewrite val_genZ [mxval _]horner_rVpoly [_ *m Ad]mulmx_sum_row. rewrite !linear_sum summx_sub // => k _. rewrite !linearZ scalemx_sub {u}//= rowK mxvecK val_gen_row. by apply: (eq_row_sub (mxvec_index i k)); rewrite rowK mxvecE mxE. 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)