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