proposition: Lemma gacts_char G M : G \subset D -> M \char R -> {acts G, on group M | to}.
proof: Proof. by move=> sGD charM; split; rewrite ?acts_char// char_sub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)