proposition: Lemma trmx_perm : forall n (s : 'S_n), (perm_mx s)^T === perm_mx s^-1.
proof: Proof. by move=> n s i j; rewrite /trmx /perm_mx (canF_eq (permK _)) eq_sym; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms