proposition: Lemma orbit1P G x : reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)).
proof: Proof. apply: (iffP afixP) => [xfix | xfix a Ga]. apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 imset_f //=. by apply/subsetP=> y; case/imsetP=> a Ga ->; rewrite inE xfix. by apply/set1P; rewrite -xfix imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)