replace h1 : f 0 = 0 := by
  contrapose! h0; rw [← zero_lt_iff] at h0
  obtain ⟨K, h2⟩ := exists_sup_fn_fin f (f 0)
  refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
  rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
  exact h2 _ (Nat.mod_lt (f (K + K + 1)) h0)
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f = fun x => x
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ f = fun x => x