Theorem: onePlusOneAndLessThan (Fpil/Chap03/Sec00.lean)

State before:
⊢ 1 + 1 = 2 ∨ 3 < 5
Tactic:
simp
State after:
no goals