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