DEFINITION minus_x_SO()
TYPE =
       ∀x:nat.(lt O x)→(eq nat x (S (minus x (S O))))
BODY =
Show proof