proposition: Lemma similar0 m (A : 'M[R]_0) (B : 'M[R]_m) : (0 = m)%N -> similar A B.
proof: Proof. move=> H; split=> //. exists 1%:M; first exact: unitmx1. by apply/matrixP; case. Qed.
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