have ⟨k₁, hk⟩ : ∃ k, k₁' = k + k₂ := by
  rw [← le_iff_exists_add']
  obtain ⟨_, h₂⟩ := h
  simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] 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 left.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 (left 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₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
case left.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 (left 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₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)