import Mathlib

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