proposition: Lemma tpermJt (X : finType) (x y z : X) : x != z -> y != z -> (tperm x z ^ tperm x y)%g = tperm y z.
proof: Proof. by move=> neq_xz neq_yz; rewrite tpermJ tpermL [tperm _ _ z]tpermD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)