proposition: Lemma odd_mul_tperm x y s : odd_perm (tperm x y * s) = (x != y) (+) odd_perm s.
proof: Proof. rewrite addbC -addbA -[~~ _]oddb -oddD -porbits_mul_tperm. by rewrite oddD odd_double addbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)