rwa [h1, zero_add, zero_add] at h
case a
f : ℕ → ℕ
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
h : f (0 + f x) ≤ f 0 + x
⊢ f (f x) ≤ x

case a
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
x : ℕ
⊢ x ≤ f (f x)
case a
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
x : ℕ
⊢ x ≤ f (f x)