proposition: Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b).
proof: Proof. apply/setP=> y; apply/idP/idP=> /imsetP[_ /imsetP[a Aa ->] ->{y}]. by rewrite actCJ mem_orbit ?memJ_conjg. by rewrite -actCJ mem_setact ?mem_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)