DEFINITION le_trans_S()
TYPE =
       ∀n:nat.∀m:nat.(le (S n) m)→(le n m)
BODY =
        assume n: nat
        assume m: nat
        suppose H: le (S n) m
          by (le_n .)
          we proved le n n
          by (le_S . . previous)
          we proved le n (S n)
          by (le_trans . . . previous H)
          we proved le n m
       we proved ∀n:nat.∀m:nat.(le (S n) m)→(le n m)