proposition: Lemma sub_astabQ A H Bbar : (A \subset 'C(Bbar | 'Q)) = (A \subset 'N(H)) && (A / H \subset 'C(Bbar)).
proof: Proof. rewrite astabQ -morphpreIdom subsetI; apply: andb_id2l => nHA. by rewrite -sub_quotient_pre. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)