proposition: Lemma tpermC x y a b : x != a -> y != a -> x != b -> y != b -> tperm x y * tperm a b = tperm a b * tperm x y.
proof: Proof. Proof using. move=> Hxa Hya Hxb Hyb. apply permP => i; rewrite !permM. case: (tpermP a b i) => [-> | -> |]. - by rewrite (tpermD Hxa Hya) tpermL (tpermD Hxb Hyb). - by rewrite (tpermD Hxa Hya) (tpermD Hxb Hyb) tpermR. case: (tpermP x y i) => [ _ _ _ | _ _ _ | _ _ ]. - rewrite ![y == _]eq_sym in Hya Hyb. by rewrite tpermD. - rewrite ![x == _]eq_sym in Hxa Hxb. by rewrite tpermD. - move=> /eqP; rewrite eq_sym => Hai. move=> /eqP; rewrite eq_sym => Hbi. by rewrite tpermD. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr