rw [← sub_nonneg] at h₂ ⊢
case intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  ↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂) ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂)
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₂ ≤ ↑k₁'
case intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  0 ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ 0 ≤ ↑k₁' - ↑k₂