fact: Definition similar m n (A : 'M[R]_m) (B : 'M[R]_n) := m = n /\ exists2 P, P \in unitmx & P *m A = (conform_mx P B) *m P.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring