Simple verification test: 1 + 1 = 2

import Mathlib

example : 1 + 1 = 2 := by
norm_num