proposition: Lemma similar_trans m n p (B : 'M[R]_n) (A : 'M[R]_m) (C : 'M[R]_p) : similar A B -> similar B C -> similar A C.
proof: Proof. case=> [Hmn HAB] [Hnp]. move: Hmn Hnp A B C HAB=> -> -> A B C [P HP HAB] [Q HQ HBC]. split=> //; exists (Q *m P); first by rewrite unitmx_mul HP HQ. by rewrite -mulmxA HAB !conform_mx_id !mulmxA HBC conform_mx_id. 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