proposition: Lemma mul_row_col m n1 n2 p (Al : 'M_(m, n1)) (Ar : 'M_(m, n2)) (Bu : 'M_(n1, p)) (Bd : 'M_(n2, p)) : row_mx Al Ar *m col_mx Bu Bd = Al *m Bu + Ar *m Bd.
proof: Proof. apply/matrixP=> i k; rewrite !mxE big_split_ord /=. congr (_ + _); apply: eq_bigr => j _; first by rewrite row_mxEl col_mxEu. by rewrite row_mxEr col_mxEd. 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)