replace h0 : ∀ x : ℕ, f (f x) = x := by
  intros x; apply le_antisymm
  replace h := h x 0
  rwa [h1, zero_add, zero_add] at h
  replace h0 := h0 x 0
  rwa [h1, zero_add, zero_add] at 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 : f 0 = 0
⊢ f = fun x => x
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
⊢ f = fun x => x