def onePlusOneIsThree : 1 + 1 = 3 := rfl
