DEFINITION lt()
TYPE =
       nat→nat→Prop
BODY =
λn:nat.λm:nat.le (S n) m