proposition: Lemma modact_is_action : is_action (D / H) modact.
proof: Proof. split=> [Ha x y | x Ha Hb]; last first. case/morphimP=> a Na Da ->{Ha}; case/morphimP=> b Nb Db ->{Hb}. rewrite -morphM //= !modactEcond // ?groupM ?(introT setIP _) //. by case: ifP => Cx; rewrite ?(acts_dom, Cx, actMin, introT setIP _). case: (set_0Vmem (D :&: Ha)) => [Da0 | [a /setIP[Da NHa]]]. by rewrite /modact Da0 repr_set0 !act1 !if_same. have Na := subsetP (coset_norm _) _ NHa. have NDa: a \in 'N_D(H) by rewrite inE Da. rewrite -(coset_mem NHa) !modactEcond //. do 2![case: ifP]=> Cy Cx // eqxy; first exact: act_inj eqxy. by rewrite -eqxy acts_dom ?Cx in Cy. by rewrite eqxy acts_dom ?Cy in Cx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)