proposition: Lemma tpermJ (T : finType) x y (s : {perm T}) : (tperm x y) ^ s = tperm (s x) (s y).
proof: Proof. by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)