proposition: Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
proof: Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)