constructor
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b ↔ (a < x ∧ x ≤ c) ∧ (b < x → c < x)
case a.mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ a < x ∧ x ≤ b → (a < x ∧ x ≤ c) ∧ (b < x → c < x)

case a.mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ (a < x ∧ x ≤ c) ∧ (b < x → c < x) → a < x ∧ x ≤ b