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))