-- NATths

theorems:

  suc(x) > 0
& suc(x) > x
& (Nat(x) ===> x = 0 | Any y:(x = suc(y) & Nat(y)))
& 0+x = x
& suc(x) + y = suc(x+y)
& (suc(x) < y+y <=== suc(x) < suc(y))
& (suc(x-suc(y)) = x-y <=== x > y)
& (x*suc(y))+(z-x) = (x*y)+z
& (x >= suc(y) ===> x > y)
& (x > y ===> x >= y)
& 2*x = x+x

--& (p+x = b & q+x = c     <=== p+x = b & q-p = c-b)
--& (p+x = b & q+(a*x) = c <=== p+x = b & q-(a*p) = c-(a*b))
--& (p+x = b & q-x = c     <=== p+x = b & q+p = c+b)
--& (p+x = b & q-(a*x) = c <=== p+x = b & q+(a*p) = c+(a*b))

& (a+x = b <=== x = b-a)

& (even(x) | odd(x) <=== Nat(x))