DEFINITION le_trans_plus_r()
TYPE =
       ∀x:nat.∀y:nat.∀z:nat.(le (plus x y) z)→(le y z)
BODY =
        assume x: nat
        assume y: nat
        assume z: nat
        suppose H: le (plus x y) z
          by (le_plus_r . .)
          we proved le y (plus x y)
          by (le_trans . . . previous H)
          we proved le y z
       we proved ∀x:nat.∀y:nat.∀z:nat.(le (plus x y) z)→(le y z)