proposition: Lemma tperm_on x y : perm_on [set x; y] (tperm x y).
proof: Proof. by apply/subsetP => z /[!inE]; case: tpermP => [->|->|]; rewrite eqxx // orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)