proposition: Lemma mul_block_col m1 m2 n1 n2 p (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2)) (Adl : 'M_(m2, n1)) (Adr : 'M_(m2, n2)) (Bu : 'M_(n1, p)) (Bd : 'M_(n2, p)) : block_mx Aul Aur Adl Adr *m col_mx Bu Bd = col_mx (Aul *m Bu + Aur *m Bd) (Adl *m Bu + Adr *m Bd).
proof: Proof. by rewrite mul_col_mx !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)