proposition: Lemma acts_in_orbit A S x y : [acts A, on S | to] -> y \in orbit to A x -> x \in S -> y \in S.
proof: Proof. by move=> nSA/imsetP[a Aa ->{y}] Sx; rewrite (astabs_act _ (subsetP nSA a Aa)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)