cases' hl with hl hl <;> push_neg at hl <;> simp 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.inl
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂

case neg.inr
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : b * (I.a₁ + I.a₂) < a * (I.b₁ + I.b₂)
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂