proposition: Lemma trmx_tperm : forall n i1 i2, (@tperm_mx n i1 i2)^T === tperm_mx i1 i2.
proof: Proof. by move=> n i1 i2; rewrite /tperm_mx; rewrite -> trmx_perm, tpermV; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms