proposition: Lemma three_subgroup G H K : [~: G, H, K] :=: 1 -> [~: H, K, G] :=: 1-> [~: K, G, H] :=: 1.
proof: Proof. move/eqP/comm3G1P=> cGHK /eqP/comm3G1P cHKG. apply/eqP/comm3G1P=> x y z Kx Gy Hz; symmetry. rewrite -(conj1g y) -(Hall_Witt_identity y^-1 z x) invgK. by rewrite cGHK ?groupV // cHKG ?groupV // !conj1g !mul1g conjgKV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)