proposition: Lemma modact_is_groupAction : is_groupAction 'C_(|to)(H) (to %% H).
proof: Proof. move=> Ha /morphimP[a Na Da ->]; have NDa: a \in 'N_D(H) by apply/setIP. rewrite inE; apply/andP; split. apply/subsetP=> x; rewrite 2!inE andbC actpermE /= modactEcond //. by apply: contraR; case: ifP => // E Rx; rewrite gact_out. apply/morphicP=> x y /setIP[Rx cHx] /setIP[Ry cHy]. rewrite /= !actpermE /= !modactE ?gactM //. suffices: x * y \in 'C_(|to)(H) by case/setIP. by rewrite groupM //; apply/setIP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)