proposition: Lemma commgAC G x y z : x \in G -> y \in G -> z \in G -> commute y z -> abelian [~: [set x], G] -> [~ x, y, z] = [~ x, z, y].
proof: Proof. move=> Gx Gy Gz cyz /centsP cRxG; pose cx' u := [~ x^-1, u]. have xR3 u v: [~ x, u, v] = x^-1 * (cx' u * cx' v) * x ^ (u * v). rewrite mulgA -conjg_mulR conjVg [cx' v]commgEl mulgA -invMg. by rewrite -mulgA conjgM -conjMg -!commgEl. suffices RxGcx' u: u \in G -> cx' u \in [~: [set x], G]. by rewrite !xR3 {}cyz; congr (_ * _ * _); rewrite cRxG ?RxGcx'. move=> Gu; suffices/groupMl <-: [~ x, u] ^ x^-1 \in [~: [set x], G]. by rewrite -commMgJ mulgV comm1g group1. by rewrite memJ_norm ?mem_commg ?set11 // groupV (subsetP (commg_normr _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)