simp at h₁ h₂
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
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
⊢ mem a b I