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