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