proposition: Lemma mulmxA m n p q (A : 'M_(m, n)) (B : 'M_(n, p)) (C : 'M_(p, q)) : A *m (B *m C) = A *m B *m C.
proof: Proof. apply/matrixP=> i l /[!mxE]; under eq_bigr do rewrite mxE big_distrr/=. rewrite exchange_big; apply: eq_bigr => j _; rewrite mxE big_distrl /=. by under eq_bigr do rewrite mulrA. 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)