proposition: Lemma similar_equiv m n (A : 'M_m) (B : 'M_n) : similar A B -> equivalent A B.
proof: Proof. case; case: m A B; case: n => //; first by move=> A B _ _; apply: equiv0r. move=> m n A B eq [P HP HAB]. split=> //; exists P, P^-1; split=> //; first by rewrite unitmx_inv. rewrite {}HAB -mulmxA mulmxV //; move: B. by rewrite -eq=> B; rewrite !conform_mx_id mulmx1. 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