import Mathlib

theorem add_zero_simple (n : ℕ) : n + 0 = n := by
  sorry