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