proposition: Lemma comm3G1P A B C : reflect {in A & B & C, forall h k l, [~ h, k, l] = 1} ([~: A, B, C] :==: 1).
proof: Proof. have R_C := sameP trivgP commG1P. rewrite -subG1 R_C gen_subG -{}R_C gen_subG. apply: (iffP subsetP) => [cABC x y z Ax By Cz | cABC xyz]. by apply/set1P; rewrite cABC // !imset2_f. by case/imset2P=> _ z /imset2P[x y Ax By ->] Cz ->; rewrite cABC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)