proposition: Lemma trmx_rswap : forall m n (A : 'M_(m, n)) i1 i2, (rswap i1 i2 A)^T === cswap i1 i2 A^T.
proof: Proof. by rewrite/trmx/rswap/cswap=> m n A i1 i2 i j; case tpermP; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms