import Base

import Nat

import UIntDefs

import UIntToFrom

import UIntLess

toNat_add: (all x:UInt, y:UInt. toNat(x + y) = toNat(x) + toNat(y))

uint_add_commute: (all x:UInt, y:UInt. x + y = y + x)

uint_add_assoc: (all x:UInt, y:UInt, z:UInt. (x + y) + z = x + (y + z))

uint_zero_add: (all x:UInt. 0 + x = x)

uint_add_zero: (all x:UInt. x + 0 = x)

uint_zero_less_one_add: (all n:UInt. 0 < 1 + n)

uint_add_both_sides_of_equal: (all x:UInt, y:UInt, z:UInt. ((x + y = x + z) ⇔ (y = z)))

uint_add_to_zero: (all n:UInt, m:UInt. (if n + m = 0 then (n = 0 and m = 0)))

uint_less_equal_add: (all x:UInt, y:UInt. x ≤ x + y)

uint_less_add_pos: (all x:UInt, y:UInt. (if 0 < y then x < x + y))