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