proposition: Lemma tperm_braid x y z : x != y -> y != z -> tperm x y * tperm y z * tperm x y = tperm y z * tperm x y * tperm y z.
proof: Proof. Proof using. move=> Hxy Hyz. rewrite -{1}(tpermV x y) -mulgA -/(conjg _ _) tpermJ tpermR. rewrite -{1}(tpermV y z) -mulgA -/(conjg _ _) tpermJ tpermL. case: (x =P z) => [-> | /eqP Hxz]. - by rewrite tpermR tpermL tpermC. - rewrite (tpermD Hxz Hyz). rewrite ![x == _]eq_sym in Hxy Hxz. by rewrite (tpermD Hxy Hxz). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr