Theorems about Successor

This short file gives the theorems which rely only on successor and predecessor functions.

 ** Module lib_nat_suc_thms Imports lib_nat
  Eq_resp_suc = ... : {m,n|nat}(Eq m n)->Eq (suc m) (suc n)
  Eq_resp_pred = ... : {m,n|nat}(Eq m n)->Eq (pred m) (pred n)
  suc_injective = ... : {m,n|nat}(Eq (suc m) (suc n))->Eq m n
  n_not_suc_n = ... : {n:nat}not (Eq n (suc n))
  suc_pred = ... : {n|nat}(not (Eq n zero))->Eq n (suc (pred n))