DEFINITION lt_plus_minus()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(eq nat y (S (plus x (minus y (S x)))))
BODY =
        assume x: nat
        assume y: nat
        suppose H: lt x y
          consider H
          we proved lt x y
          that is equivalent to le (S x) y
          by (le_plus_minus . . previous)
          we proved eq nat y (plus (S x) (minus y (S x)))
          that is equivalent to eq nat y (S (plus x (minus y (S x))))
       we proved 
          ∀x:nat.∀y:nat.(lt x y)→(eq nat y (S (plus x (minus y (S x)))))