DEFINITION lt_x_plus_x_Sy()
TYPE =
       ∀x:nat.∀y:nat.(lt x (plus x (S y)))
BODY =
Show proof