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