DEFINITION le_n_pred()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(le (pred n) (pred m))
BODY =
Show proof