proposition: Lemma tperm_proof x y : involutive [fun z => z with x |-> y, y |-> x].
proof: Proof. move=> z /=; case: (z =P x) => [-> | ne_zx]; first by rewrite eqxx; case: eqP. by case: (z =P y) => [->| ne_zy]; [rewrite eqxx | do 2?case: eqP]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)