DEFINITION lt_O_Sn()
TYPE =
       ∀n:nat.(lt O (S n))
BODY =
Show proof