rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
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
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 (f (K + K + 1) % f 0) ≤ K