proposition: Lemma afix_mod G S : H \subset 'C(S | to) -> G \subset 'N_D(H) -> 'Fix_(S | mod_action)(G / H) = 'Fix_(S | to)(G).
proof: Proof. move=> cSH /subsetIP[sGD nHG]. apply/eqP; rewrite eqEsubset !subsetI !subsetIl /= -!astabCin ?quotientS //. have cfixH F: H \subset 'C(S :&: F | to). by rewrite (subset_trans cSH) // astabS ?subsetIl. rewrite andbC astab_mod ?quotientS //=; last by rewrite astabCin ?subsetIr. by rewrite -(quotientSGK nHG) //= -astab_mod // astabCin ?quotientS ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)