proposition: Lemma actby_is_groupAction : is_groupAction G <[nGAg]>.
proof: Proof. move=> a Aa; rewrite /= inE; apply/andP; split. apply/subsetP=> x; apply: contraR => Gx. by rewrite actpermE /= /actby (negbTE Gx). apply/morphicP=> x y Gx Gy; rewrite !actpermE /= /actby Aa groupM ?Gx ?Gy //=. by case nGAg; move/acts_dom; do 2!move/subsetP=> ?; rewrite gactM; auto. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)