proposition: Lemma equiv_refl m n (A : 'M[R]_(m,n)) : equivalent A A.
proof: Proof. split=> //; exists 1%:M, 1%:M. by split; rewrite ?unitmx1 // conform_mx_id mulmx1 mul1mx. 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