exact ⟨h₂, h₁.2⟩
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
x✝ : (a < x ∧ x ≤ c) ∧ (b < x → c < x)
h₁ : a < x ∧ x ≤ c
h₂ : b < x
⊢ b < x ∧ x ≤ c
no goals