DEFINITION le_plus_trans()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(le n m)→(le n (plus m p))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        suppose H: le n m
          by (le_plus_l . .)
          we proved le m (plus m p)
          by (le_trans . . . H previous)
          we proved le n (plus m p)
       we proved ∀n:nat.∀m:nat.∀p:nat.(le n m)→(le n (plus m p))