proposition: Lemma eq_fullrowsub : (rowsub frf A :=: A)%MS.
proof: Proof. rewrite mxsub_ffunl rowsub_comp rowsub_cast esymK. exact: (eqmx_trans (eqmx_cast _ _) eq_maxrowsub). 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)