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