proposition: Lemma atransPin G S : G \subset D -> [transitive G, on S | to] -> forall x, x \in S -> orbit to G x = S.
proof: Proof. by move=> sGD /imsetP[y _ ->] x; apply/orbit_in_eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)