refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ ∃ x y, f y + f (y + f x) < x
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (0 + f (K + K + 1)) ≤ K