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