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