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