import Mathlib

theorem nat_add_zero_identity (n : ℕ) : n + 0 = n := by
  rfl