import Mathlib

example : 1 + 1 = 2 := by
norm_num