simp only [mem_interior] at h
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : mem_interior a b I
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂