DEFINITION lt_n_S()
TYPE =
       ∀n:nat.∀m:nat.(lt n m)→(lt (S n) (S m))
BODY =
Show proof