proposition: Lemma morphim_actm : {in D, forall a (S : {set rT}), S \subset R -> actm to a @* S = to^* S a}.
proof: Proof. by move=> a Da /= S sSR; rewrite /morphim /= actmEfun ?(setIidPr _). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)