convert h₁ using 1
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₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑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
⊢ 0 ≤ ↑k₂' - ↑k₁
case h.e'_4
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₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑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₁ =
    ↑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₂))