less_equal_fromNat: (all x:Nat, y:Nat. (if x ≤ y then fromNat(x) ≤ fromNat(y)))

less_equal_toNat: (all x:UInt, y:UInt. (if toNat(x) ≤ toNat(y) then x ≤ y))

less_fromNat: (all x:Nat, y:Nat. (if x < y then fromNat(x) < fromNat(y)))

less_toNat: (all x:UInt, y:UInt. (if toNat(x) < toNat(y) then x < y))

toNat_less: (all x:UInt, y:UInt. (if x < y then toNat(x) < toNat(y)))

toNat_less_equal: (all x:UInt, y:UInt. (if x ≤ y then toNat(x) ≤ toNat(y)))

uint_bzero_le: (all x:UInt. bzero ≤ x)

uint_dichotomy: (all x:UInt, y:UInt. (x ≤ y or y < x))

uint_equal_implies_less_equal: (all x:UInt, y:UInt. (if x = y then x ≤ y))

uint_less_equal_antisymmetric: (all x:UInt, y:UInt. (if (x ≤ y and y ≤ x) then x = y))

uint_less_equal_refl: (all n:UInt. n ≤ n)

auto uint_less_equal_refl_true

uint_less_equal_refl_true: (all n:UInt. (n ≤ n) = true)

uint_less_equal_trans: (all x:UInt, y:UInt, z:UInt. (if (x ≤ y and y ≤ z) then x ≤ z))

uint_less_equal_zero: (all x:UInt. (if x ≤ 0 then x = 0))

uint_less_implies_less_equal: (all x:UInt, y:UInt. (if x < y then x ≤ y))

uint_less_implies_not_greater: (all x:UInt, y:UInt. (if x < y then not (y < x)))

uint_less_irreflexive: (all x:UInt. not (x < x))

auto uint_less_refl_false

uint_less_refl_false: (all x:UInt. (x < x) = false)

uint_less_trans: (all x:UInt, y:UInt, z:UInt. (if (x < y and y < z) then x < z))

auto uint_lit_less

uint_lit_less: (all x:Nat, y:Nat. (fromNat(lit(x)) < fromNat(lit(y))) = (lit(x) < lit(y)))

auto uint_lit_less_equal

uint_lit_less_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) ≤ fromNat(lit(y))) = (lit(x) ≤ lit(y)))

uint_max_assoc: (all x:UInt, y:UInt, z:UInt. max(max(x, y), z) = max(x, max(y, z)))

uint_max_equal_greater_left: (all x:UInt, y:UInt. (if y ≤ x then max(x, y) = x))

uint_max_equal_greater_right: (all x:UInt, y:UInt. (if x ≤ y then max(x, y) = y))

uint_max_less_equal: (all x:UInt, y:UInt, z:UInt. (if (x ≤ z and y ≤ z) then max(x, y) ≤ z))

uint_max_symmetric: (all x:UInt, y:UInt. max(x, y) = max(y, x))

uint_max_zero: (all x:UInt. max(x, 0) = x)

uint_not_less_equal_iff_greater: (all x:UInt, y:UInt. (not (x ≤ y) ⇔ (y < x)))

uint_not_less_implies_less_equal: (all x:UInt, y:UInt. (if not (x < y) then y ≤ x))

uint_not_less_zero: (all x:UInt. not (x < 0))

uint_trichotomy: (all x:UInt, y:UInt. (x < y or x = y or y < x))

uint_zero_le: (all x:UInt. 0 ≤ x)

auto uint_zero_less_equal_true

uint_zero_less_equal_true: (all x:UInt. (0 ≤ x) = true)

uint_zero_max: (all x:UInt. max(0, x) = x)

uint_zero_or_positive: (all x:UInt. (x = 0 or 0 < x))