DEFINITION lt_x_pred_y()
TYPE =
       ∀x:nat.∀y:nat.(lt x (pred y))→(lt (S x) y)
BODY =
Show proof