by_cases h : 0 < n
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
⊢ n = 0
case pos
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : 0 < n
⊢ n = 0

case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0