proposition: Lemma stable_row_base f : (row_base V *m f <= row_base V)%MS = (V *m f <= V)%MS.
proof: Proof. rewrite eq_row_base. by apply/idP/idP=> /(submx_trans _) ->; rewrite ?submxMr ?eq_row_base. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)