proposition: Lemma conj_astabQ A H x : x \in 'N(H) -> 'C(A / H | 'Q) :^ x = 'C(A :^ x / H | 'Q).
proof: Proof. move=> nHx; apply/setP=> y; rewrite !astabQ mem_conjg !in_setI -mem_conjg. rewrite -normJ (normP nHx) quotientJ //; apply/andb_id2l => nHy. by rewrite !inE centJ morphJ ?groupV ?morphV // -mem_conjg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)