fromNat_add: (all x:Nat, y:Nat. fromNat(x + y) = fromNat(x) + fromNat(y))

auto lit_add_fromNat

lit_add_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) + fromNat(lit(y)) = fromNat(lit(x) + lit(y)))

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

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

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

auto uint_add_both_sides_of_le_equal

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

uint_add_both_sides_of_less: (all x:UInt, y:UInt, z:UInt. ((x + y < x + z)  (y < z)))

uint_add_both_sides_of_less_equal: (all x:UInt. (all y:UInt, z:UInt. ((x + y  x + z)  (y  z))))

auto uint_add_bzero

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

uint_add_mono_less: (all a:UInt, b:UInt, c:UInt, d:UInt. (if (a < c and b < d) then a + b < c + d))

uint_add_mono_less_equal: (all a:UInt, b:UInt, c:UInt, d:UInt. (if (a  c and b  d) then a + b  c + d))

uint_add_one_le_double: (all x:UInt. (if 0 < x then 1 + x  x + x))

uint_add_to_bzero: (all n:UInt, m:UInt. (if n + m = bzero then (n = bzero and m = bzero)))

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

auto uint_add_zero

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

auto uint_bzero_add

uint_bzero_less_one_add: (all n:UInt. bzero < 1 + n)

uint_induction: (all P:(fn UInt -> bool). (if (P(0) and (all m:UInt. (if P(m) then P(1 + m)))) then (all n:UInt. P(n))))

uint_k_induction: (all P:(fn UInt -> bool), k:UInt. (if (P(k) and (all m:UInt. (if P(m) then P(1 + m)))) then (all n:UInt. (if k  n then P(n)))))

uint_less_add_one_implies_less_equal: (all x:UInt, y:UInt. (if x < 1 + y then x  y))

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

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

uint_less_equal_add_left: (all x:UInt, y:UInt. y  x + y)

uint_less_is_less_equal: (all x:UInt, y:UInt. (x < y) = (1 + x  y))

uint_less_plus1: (all n:UInt. n < 1 + n)

auto uint_less_plus1_true

uint_less_plus1_true: (all n:UInt. (n < 1 + n) = true)

uint_not_one_add_le_zero: (all n:UInt. not (1 + n  0))

uint_not_one_add_zero: (all n:UInt. not (1 + n = 0))

uint_not_zero_pos: (all n:UInt. (if not (n = 0) then 0 < n))

auto uint_one_add_zero_false

uint_one_add_zero_false: (all n:UInt. (1 + n = 0) = false)

uint_pos_implies_one_le: (all n:UInt. (if 0 < n then 1  n))

uint_pos_not_zero: (all n:UInt. (if 0 < n then not (n = 0)))

uint_positive_add_one: (all n:UInt. (if 0 < n then some n':UInt. n = 1 + n'))

auto uint_zero_add

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

uint_zero_le_zero: (all x:UInt. (if x  0 then x = 0))

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

auto uint_zero_less_one_add_true

uint_zero_less_one_add_true: (all n:UInt. (0 < 1 + n) = true)

uint_zero_or_add_one: (all x:UInt. (x = 0 or some x':UInt. x = 1 + x'))