DEFINITION lt_plus_minus_r()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(eq nat y (S (plus (minus y (S x)) x)))
BODY =
        assume x: nat
        assume y: nat
        suppose H: lt x y
          (h1) 
             by (lt_plus_minus . . H)
eq nat y (S (plus x (minus y (S x))))
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus (minus y (S x)) x) (plus x (minus y (S x)))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat y (S (plus (minus y (S x)) x))
       we proved 
          ∀x:nat.∀y:nat.(lt x y)→(eq nat y (S (plus (minus y (S x)) x)))