no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ cycleType σ
⊢ 2 ∣ n
rw [le_antisymm
    (Nat.le_of_dvd zero_lt_two <|
      (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
    (two_le_of_mem_cycleType hn)]