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