α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : a ≤ x ∧ x < b
hbc : c ≤ x ∧ x < d
⊢ False
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : x ∈ Ico a b
hbc : x ∈ Ico c d
⊢ False
rw [mem_Ico] at hab hbc
no goals
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : a ≤ x ∧ x < b
hbc : c ≤ x ∧ x < d
⊢ False
exact hab.2.not_le (h.trans hbc.1)