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