DEFINITION le_plus_minus_r()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(eq nat (plus n (minus m n)) m)
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          by (le_plus_minus . . H)
          we proved eq nat m (plus n (minus m n))
          by (sym_eq . . . previous)
          we proved eq nat (plus n (minus m n)) m
       we proved ∀n:nat.∀m:nat.(le n m)→(eq nat (plus n (minus m n)) m)