proposition: Lemma Hall_Witt_identity x y z : [~ x, y^-1, z] ^ y * [~ y, z^-1, x] ^ z * [~ z, x^-1, y] ^ x = 1.
proof: Proof. pose a x y z : gT := x * z * y ^ x. suffices{x y z} hw_aux x y z: [~ x, y^-1, z] ^ y = (a x y z)^-1 * (a y z x). by rewrite !hw_aux 2!mulgA !mulgK mulVg. by rewrite commgEr conjMg -conjgM -conjg_Rmul 2!invMg conjgE !mulgA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)