proposition: Lemma conform_castmx m1 n1 m2 n2 m3 n3 (e_mn : (m2 = m3) * (n2 = n3)) (B : 'M_(m1, n1)) A : conform_mx B (castmx e_mn A) = conform_mx B A.
proof: Proof. by do [case: e_mn; case: m3 /; case: n3 /] in A *. 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)