rw [@not_and_or] at hl
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₂
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₂