calc
  d < I.a₁ + I.a₂ + I.b₁ + I.b₂                       := hI.2.2
  _ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)                     := by abel
  _ ≤ k₁ * (I.a₁ + I.b₁) + k₂ * (I.a₂ + I.b₂)         :=
    Nat.add_le_add (Nat.le_mul_of_pos_left _ hk₁) (Nat.le_mul_of_pos_left _ hk₂)
  _ = k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂) := by ring
  _ = a + b                                           := by rw [h₁, h₂]
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
no goals