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