proposition: Lemma gactM : {in D, forall a, {in R &, {morph to^~ a : x y / x * y}}}.
proof: Proof. move=> a Da /= x y; rewrite -!(actpermE to); apply: morphicP x y. by rewrite Aut_morphic ?actperm_Aut. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)