refine Or.inr ⟨hl.le, h.2⟩
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₂
no goals