zify at h₁ rel ⊢
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₁ :
  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
⊢ 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₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  ↑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
⊢ ↑k₁ ≤ ↑k₂'