proposition: Lemma acts_char G M : G \subset D -> M \char R -> [acts G, on M | to].
proof: Proof. move=> sGD /charP[sMR charM]. apply/subsetP=> a Ga; have Da := subsetP sGD a Ga; rewrite !inE Da. apply/subsetP=> x Mx; have Rx := subsetP sMR x Mx. by rewrite inE -(charM _ (injm_actm a) (im_actm a)) -actmE // mem_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)