DEFINITION lt_plus_minus_r()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(eq nat y (S (plus (minus y (S x)) x)))
BODY =
Show proof