proposition: Lemma acts_sub_orbit G S x : [acts G, on S | to] -> (orbit to G x \subset S) = (x \in S).
proof: Proof. move/acts_act=> GactS. apply/subsetP/idP=> [| Sx y]; first by apply; apply: orbit_refl. by case/orbitP=> a Ga <-{y}; rewrite GactS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)