have rel := I.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₂
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₂)
⊢ 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₂ :
  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₁'