DEFINITION le_plus_minus_sym()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(eq nat m (plus (minus m n) n))
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          (h1) 
             by (le_plus_minus . . H)
eq nat m (plus n (minus m n))
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus (minus m n) n) (plus n (minus m n))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat m (plus (minus m n) n)
       we proved ∀n:nat.∀m:nat.(le n m)→(eq nat m (plus (minus m n) n))