obtain ⟨h₁, h₂⟩ := h
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I