import Mathlib

example : 1 + 1 = 3 := by
norm_num