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_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_greater_implies_not_equal: (all x:UInt, y:UInt. (if x > y then not (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_equal: (all x:UInt, y:UInt. (if x < y then not (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_greater_left: (all x:UInt, y:UInt. x ≤ max(x, y))

uint_max_greater_right: (all x:UInt, y:UInt. y ≤ max(x, y))

uint_max_idempotent: (all x:UInt. max(x, x) = x)

uint_max_is_left_or_right: (all x:UInt, y:UInt. ((max(x, y) = x) or (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_min_absorb_left: (all x:UInt, y:UInt. max(x, min(x, y)) = x)

uint_max_min_absorb_right: (all x:UInt, y:UInt. max(min(x, y), x) = x)

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

auto uint_max_zero

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

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

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

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

uint_min_idempotent: (all x:UInt. min(x, x) = x)

uint_min_is_left_or_right: (all x:UInt, y:UInt. ((min(x, y) = x) or (min(x, y) = y)))

uint_min_less_equal_left: (all x:UInt, y:UInt. min(x, y) ≤ x)

uint_min_less_equal_right: (all x:UInt, y:UInt. min(x, y) ≤ y)

uint_min_max_absorb_left: (all x:UInt, y:UInt. min(x, max(x, y)) = x)

uint_min_max_absorb_right: (all x:UInt, y:UInt. min(max(x, y), x) = x)

uint_min_symmetric: (all x:UInt, y:UInt. min(x, y) = min(y, 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)

auto uint_zero_max

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

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