proposition: Lemma stablemx_restrict m n (A : 'M[F]_n) (V : 'M_n) (W : 'M_(m, \rank V)): stablemx V A -> stablemx W (restrictmx V A) = stablemx (W *m row_base V) A.
proof: Proof. move=> A_stabV; rewrite mulmxA -[in RHS]mulmxA. rewrite -(submxMfree _ W (row_base_free V)) mulmxKpV //. by rewrite mulmx_sub ?stablemx_row_base. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)