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

inc_add_one: (all n:UInt. inc(n) = 1 + n)

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))))

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_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)

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 ((k ≤ m) and 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_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'))

uint_strong_induction: (all P:(fn UInt -> bool), n:UInt. (if (all j:UInt. (if (all i:UInt. (if i < j then P(i))) then P(j))) then P(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'))