proposition: Lemma equiv_trans m1 n1 m2 n2 m3 n3 (B : 'M[R]_(m2,n2)) (A : 'M[R]_(m1,n1)) (C : 'M[R]_(m3,n3)) : equivalent A B -> equivalent B C -> equivalent A C.
proof: Proof. case=> eqm12 eqn12 [M1 [N1 [HM1 HN1 HAB]]]. case=> eqm23 eqn23 [M2 [N2 [HM2 HN2 HBC]]]. split; [exact: (etrans eqm12) | exact: (etrans eqn12)|]. move: A B M1 N1 M2 N2 HM1 HN1 HM2 HN2 HAB HBC. rewrite eqm12 eqn12 eqm23 eqn23=> A B M1 N1 M2 N2 HM1 HN1 HM2 HN2. rewrite !conform_mx_id=> HAB HBC. exists (M2 *m M1), (N1 *m N2); split; try by rewrite unitmx_mul; apply/andP. by rewrite -!(mulmxA M2) (mulmxA (_ *m A)) HAB mulmxA. 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