proposition: Lemma mul_tperm_mx : forall m n (A : 'M_(m, n)) i1 i2, (tperm_mx i1 i2) *m A === rswap i1 i2 A.
proof: Proof. move=> m n' A i1 i2 i j. rewrite /mulmx /tperm_mx /perm_mx /rswap. setoid_rewrite (bigD1 (j:=tperm i1 i2 i))=>//=. setoid_rewrite (big1 (P:=fun k => k != tperm i1 i2 i))=>[|k]; first by rewrite eq_refl; ring. by rewrite eq_sym; move/negbTE => ->; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms