unfold mem at h hl ⊢
case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬(b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂)
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂