DEFINITION le_pred_n()
TYPE =
       ∀n:nat.(le (pred n) n)
BODY =
Show proof