ι : Type ?u.46031
α : Type u
β : Type v
γ : Type w
δ : Type ?u.46040
π : ι → Type ?u.46045
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
ι : Type ?u.46031
α : Type u
β : Type v
γ : Type w
δ : Type ?u.46040
π : ι → Type ?u.46045
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x
rintro rfl
no goals
ι : Type ?u.46031
α : Type u
β : Type v
γ : Type w
δ : Type ?u.46040
π : ι → Type ?u.46045
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)