proposition: Lemma orbit_morphim_actperm (A : {set aT}) : A \subset D -> orbit 'P (actperm to @* A) =1 orbit to A.
proof: Proof. move=> sAD x; rewrite morphimEsub // /orbit -imset_comp. by apply: eq_imset => a //=; rewrite actpermK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)