obtain ⟨k₁, k₂', H₁, H₂⟩ := ih (mem_of_mem_right I h)
case right
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 (right I)
⊢ ∃ k₁ k₂, a = k₁ * (right I).a₁ + k₂ * (right I).a₂ ∧ b = k₁ * (right I).b₁ + k₂ * (right I).b₂
case right.intro.intro.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₂
h : mem a b (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (right I).a₁ + k₂ * (right I).a₂ ∧ b = k₁ * (right I).b₁ + k₂ * (right I).b₂