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