have ⟨k₂, hk⟩ : ∃ k, k₂' = k + k₁ := by
  rw [← le_iff_exists_add']
  obtain ⟨h₁, _⟩ := h
  simp only [H₂, right_a₁, mul_add, add_mul, H₁, right_b₁] at h₁
  have rel := I.rel
  zify at h₁ rel ⊢
  rw [← sub_nonneg] at h₁ ⊢
  convert h₁ using 1
  linear_combination (k₁ - k₂') * rel
  done
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₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * 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₂ : ℕ
hk : k₂' = k₂ + k₁
⊢ ∃ k₁ k₂, a = k₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂