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