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