Theorems about Minus

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