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