proposition: Lemma modactEcond x a : a \in dom -> modact x (coset H a) = (if x \in range then to x a else x).
proof: Proof. case/setIP=> Da Na; case: ifP => Cx; rewrite /modact Cx //. rewrite val_coset // -group_modr ?sub1set //. case: (repr _) / (repr_rcosetP (D :&: H) a) => a' Ha'. by rewrite actMin ?(afixP Cx _ Ha') //; case/setIP: Ha'. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)