proposition: Lemma rowsubE m m' n f (A : 'M_(m, n)) : rowsub f A = rowsub f 1%:M *m A :> 'M_(m', n).
proof: Proof. by rewrite mul_rowsub_mx mul1mx. 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 countalg finalg zmodp)