proposition: Lemma rowsub_comp m1 m2 m3 n (f : 'I_m2 -> 'I_m1) (f' : 'I_m3 -> 'I_m2) (A : 'M_(m1, n)) : rowsub (f \o f') A = rowsub f' (rowsub f A).
proof: Proof. exact: mxsub_comp. 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)