proposition: Lemma astab_mod : 'C(S | mod_action) = 'C(S | to) / H.
proof: Proof. apply/setP=> Ha; apply/idP/morphimP=> [cSa | [a nHa cSa ->]]. case/morphimP: (astab_dom cSa) => a nHa Da defHa. exists a => //; rewrite !inE Da; apply/subsetP=> x Sx; rewrite !inE. by rewrite -{2}[x](astab_act cSa) // defHa /= modactE ?(subsetP fixSH). have Da := astab_dom cSa; rewrite !inE mem_quotient //; apply/subsetP=> x Sx. by rewrite !inE /= modactE ?(astab_act cSa) ?(subsetP fixSH). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)