proposition: Lemma map2_conform_mx m' n' (A' : 'M_(m', n')) (B' : 'M_(m', n')) : map2_mx (conform_mx A' A) (conform_mx B' B) = conform_mx (map2_mx A' B') (map2_mx A B).
proof: Proof. move: A' B'; have [[<- <-] A' B'|] := eqVneq (m, n) (m', n'). by rewrite !conform_mx_id. by rewrite negb_and => neq_mn A' B'; rewrite !nonconform_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)