Transitivity from cyclic rotation

A permutation subgroup containing cyclic rotation acts transitively on the finite ordinal. This gives a transitivity criterion for groups specified by generators, including the empty and singleton ordinals.

theorem TauCeti.isPretransitive_of_finRotate_mem {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (hg : finRotate n ∈ G) : MulAction.IsPretransitive (↥G) (Fin n)

A permutation subgroup containing cyclic rotation acts transitively.