obtain ⟨k₁, k₂, hk₁, hk₂, h₁, h₂⟩ := exists_of_mem_interior hab
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
⊢ d < a + b
case intro.intro.intro.intro.intro
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ d < a + b