proposition: Lemma gacent_mod G M : H \subset 'C(M | to) -> G \subset 'N(H) -> 'C_(M | mod_groupAction)(G / H) = 'C_(M | to)(G).
proof: Proof. move=> cMH nHG; rewrite -gacentIdom gacentE ?subsetIl // setICA. have sHD: H \subset D by rewrite (subset_trans cMH) ?subsetIl. rewrite -quotientGI // afix_mod ?setIS // setICA -gacentIim (setIC R) -setIA. rewrite -gacentE ?subsetIl // gacentIdom setICA (setIidPr _) //. by rewrite gacentC // ?(subset_trans cMH) ?astabS ?subsetIl // setICA subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)