proposition: Lemma nonconform_mx m m' n n' (B : 'M_(m', n')) (A : 'M_(m, n)) : (m != m') || (n != n') -> conform_mx B A = B.
proof: Proof. by rewrite /conform_mx; do 2!case: eqP. 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)