DEFINITION minus()
TYPE =
       nat→nat→nat
BODY =
Show proof