proposition: Lemma orbit_partition G S : [acts G, on S | to] -> partition (orbit to G @: S) S.
proof: Proof. move=> actsGS; have sGD := acts_dom actsGS. have eqiG: {in S & &, equivalence_rel [rel x y | y \in orbit to G x]}. by move=> x y z * /=; rewrite orbit_refl; split=> // /orbit_in_eqP->. congr (partition _ _): (equivalence_partitionP eqiG). apply: eq_in_imset => x Sx; apply/setP=> y. by rewrite inE /= andb_idl // => /acts_in_orbit->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)