DEFINITION plus_minus()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat n (plus m p))→(eq nat p (minus n m))
BODY =
Show proof