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