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