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