DEFINITION le_trans_plus_r()
TYPE =
       ∀x:nat.∀y:nat.∀z:nat.(le (plus x y) z)→(le y z)
BODY =
Show proof