theorem add_zero_demo (n : Nat) : n + 0 = n := by simp