proposition: Lemma equiv_sym m1 n1 m2 n2 (A : 'M[R]_(m1,n1)) (B : 'M[R]_(m2,n2)) : equivalent A B -> equivalent B A.
proof: Proof. case: m2 A B=> [A B [eq1 eq2 _]|]; first by apply/equiv0l/esym. case: n2=> [m2 A B [eq1 eq2 _]|]; first by apply/equiv0r/esym. case: m1=> [m2 n2 A B []|] //. case: n1=> [m1 m2 n2 A B []|n1 m1 n2 m2 A B [eq1 eq2 [M [N [HM HN HAB]]]]] //. split; try exact: esym. move: B HAB; rewrite -eq1 -eq2=> B; rewrite !conform_mx_id=> HAB. exists M^-1, N^-1; split; rewrite ?unitmx_inv //. by rewrite -HAB !mulmxA mulVmx // mul1mx -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