simp at h₁ h₂
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
h₂ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ mem a b I
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ mem a b I