proposition: Lemma orbit_transversalP G S (P := orbit to G @: S) (X := orbit_transversal G S) : [acts G, on S | to] -> [/\ is_transversal X P S, X \subset S, {in X &, forall x y, (y \in orbit to G x) = (x == y)} & forall x, x \in S -> exists2 a, a \in G & to x a \in X].
proof: Proof. move/orbit_partition; rewrite -/P => partP. have [/eqP defS tiP _] := and3P partP. have trXP: is_transversal X P S := transversalP partP. have sXS: X \subset S := transversal_sub trXP. split=> // [x y Xx Xy /= | x Sx]. have Sx := subsetP sXS x Xx. rewrite -(inj_in_eq (pblock_inj trXP)) // eq_pblock ?defS //. by rewrite (def_pblock tiP (imset_f _ Sx)) ?orbit_refl. have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X. by rewrite (pblock_transversal trXP) ?imset_f. suffices /orbitP[a Ga def_y]: y \in orbit to G x by exists a; rewrite ?def_y. by rewrite defxG mem_pblock defS (subsetP sXS). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)