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