proposition: Lemma similar_sym m : forall n (A : 'M[R]_m) (B : 'M[R]_n), similar A B -> similar B A.
proof: Proof. case=> [A B [H1 H2]|n A B [Hmn]]. by apply: similar0; rewrite H1. move: A; rewrite Hmn => A [P HP HPA]. split=> //; exists P^-1; first by rewrite unitmx_inv. rewrite !conform_mx_id -1?[A *m _]mul1mx -?(mulVmx HP) in HPA *. by rewrite mulmxA -(mulmxA P^-1) HPA -!mulmxA mulmxV // 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