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