proposition: Lemma astabQR A H : A \subset 'N(H) -> 'C(A / H | 'Q) = [set x in 'N(H) | [~: [set x], A] \subset H].
proof: Proof. move=> nHA; apply/setP=> x; rewrite astabQ -morphpreIdom 2!inE -astabQ. by case nHx: (x \in _); rewrite //= -sub1set sub_astabQR ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)