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