proposition: Lemma modgactE x a : H \subset 'C(R | to) -> a \in 'N_D(H) -> (to %% H)%act x (coset H a) = to x a.
proof: Proof. move=> cRH NDa /=; have [Da Na] := setIP NDa. have [Rx | notRx] := boolP (x \in R). by rewrite modactE //; apply/afixP=> b /setIP[_ /(subsetP cRH)/astab_act->]. rewrite gact_out //= /modact; case: ifP => // _; rewrite gact_out //. suffices: a \in D :&: coset H a by case/mem_repr/setIP. by rewrite inE Da val_coset // rcoset_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)