proposition: Lemma eqmx_rowsub_comp (m n p q : nat) f (g : 'I_n -> 'I_p) (A : 'M_(m, q)) : p <= n -> injective g -> (rowsub (f \o g) A :=: rowsub f A)%MS.
proof: Proof. move=> leq_pn g_inj; have eq_np : n == p by rewrite eqn_leq leq_pn (inj_leq g). rewrite (eqP eq_np) in g g_inj *. rewrite (eq_rowsub (f \o (perm g_inj))); last by move=> i; rewrite /= permE. exact: eqmx_rowsub_comp_perm. 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)