proposition: Lemma equiv0l n m p (A : 'M[R]_(0,n)) (B : 'M[R]_(m,p)) : (0 = m)%N -> (n = p)%N -> equivalent A B.
proof: Proof. move=> eq1 eq2; split=> //. exists 1%:M, 1%:M; split; try 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