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