proposition: Lemma atrans_orbit G x : [transitive G, on orbit to G x | to].
proof: Proof. by apply: imset_f; apply: orbit_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)