contrapose! h₂
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : x ≤ b
⊢ b < x → c < x
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : a < x ∧ x ≤ b
h₁ : a < x
h₂ : b < x ∧ x ≤ c
⊢ b < x