obtain ⟨_, h₂⟩ := h
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₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ 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₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ k₂ ≤ k₁'