Another small file gives a few theorems about truncated subtraction (minus).
** Module lib_nat_minus_thms Imports lib_nat_plus_thms minus_suc_pred = ... : {n,m:nat}Eq (minus n (suc m)) (minus (pred n) m) minus_resp_suc = ... : {m,n:nat}Eq (minus (suc m) (suc n)) (minus m n) n_minus_n_Eq_zero = ... : {n:nat}Eq (minus n n) zero zero_minus_n_Eq_zero = ... : {n:nat}Eq (minus zero n) zero minus_commutes_suc_l = ... : {m,n,t|nat}(Eq (minus n m) (suc t))-> Eq (minus (suc n) m) (suc (minus n m)) minus_commutes_suc_r = ... : {m,n,t|nat}(Eq (minus n m) (suc t))->Eq (minus n (suc m)) t minus_monotone_l = ... : {l:nat}{m,n,t|nat}(Eq (minus n m) (suc t))-> Eq (minus (plus n l) m) (suc (plus t l)) minus_inv_plus = ... : {m,n:nat}Eq n (minus (plus m n) m) nonzero_inv_sp = ... : {x:nat}(not (Eq x zero))->Eq (suc (pred x)) x