proposition: Lemma mul_row_block m n1 n2 p1 p2 (Al : 'M_(m, n1)) (Ar : 'M_(m, n2)) (Bul : 'M_(n1, p1)) (Bur : 'M_(n1, p2)) (Bdl : 'M_(n2, p1)) (Bdr : 'M_(n2, p2)) : row_mx Al Ar *m block_mx Bul Bur Bdl Bdr = row_mx (Al *m Bul + Ar *m Bdl) (Al *m Bur + Ar *m Bdr).
proof: Proof. by rewrite block_mxEh mul_mx_row !mul_row_col. 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)