proposition: Lemma quotient_cents2 A B K : A \subset 'N(K) -> B \subset 'N(K) -> (A / K \subset 'C(B / K)) = ([~: A, B] \subset K).
proof: Proof. move=> nKA nKB. by rewrite (sameP commG1P trivgP) /= -quotientR // quotient_sub1 // comm_subG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)