proposition: Lemma mul_mx_tperm : forall m n (A : matrix R m n) i1 i2, A *m (tperm_mx i1 i2) === cswap i1 i2 A.
proof: Proof. move=> m n A i1 i2; apply: trmx_inj. by rewrite -> trmx_mul_rev, trmx_tperm, mul_tperm_mx, trmx_cswap; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms