proposition: Lemma eqmx_stable m m' n (V : 'M[F]_(m, n)) (V' : 'M[F]_(m', n)) (f : 'M[F]_n) : (V :=: V')%MS -> stablemx V f = stablemx V' f.
proof: Proof. by move=> eqVV'; rewrite (eqmxMr _ eqVV') eqVV'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)