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