proposition: Lemma scale_block_mx m1 m2 n1 n2 a (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2)) (Adl : 'M_(m2, n1)) (Adr : 'M_(m2, n2)) : a *: block_mx Aul Aur Adl Adr = block_mx (a *: Aul) (a *: Aur) (a *: Adl) (a *: Adr).
proof: Proof. by rewrite scale_col_mx !scale_row_mx. 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)