proposition: Lemma gacentQ (gT : finGroupType) (H : {group gT}) (A : {set gT}) : 'C_(|'Q)(A) = 'C(A / H).
proof: Proof. apply/setP=> Hx; case: (cosetP Hx) => x Nx ->{Hx}. rewrite -sub_cent1 -astab1J astabC sub1set -(quotientInorm H A). have defD: qact_dom 'J H = 'N(H) by rewrite qact_domE ?subsetT ?astabsJ. rewrite !(inE, mem_quotient) //= defD setIC. apply/subsetP/subsetP=> [cAx _ /morphimP[a Na Aa ->] | cAx a Aa]. by move/cAx: Aa; rewrite !inE qactE ?defD ?morphJ. have [_ Na] := setIP Aa; move/implyP: (cAx (coset H a)); rewrite mem_morphim //. by rewrite !inE qactE ?defD ?morphJ. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)