proposition: Lemma sub_astabQR A B H : A \subset 'N(H) -> B \subset 'N(H) -> (A \subset 'C(B / H | 'Q)) = ([~: A, B] \subset H).
proof: Proof. move=> nHA nHB; rewrite sub_astabQ nHA /= (sameP commG1P eqP). by rewrite eqEsubset sub1G andbT -quotientR // quotient_sub1 // comm_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)