proposition: Lemma mul_mx_row m n p1 p2 (A : 'M_(m, n)) (Bl : 'M_(n, p1)) (Br : 'M_(n, p2)) : A *m row_mx Bl Br = row_mx (A *m Bl) (A *m Br).
proof: Proof. apply/matrixP=> i k; rewrite !mxE. by case defk: (split k) => /[!mxE]; under eq_bigr do rewrite mxE defk. 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)