union UInt

fun div2(b:UInt)

fun fromNat(Nat) -> UInt

fun log(b:UInt) {
  cnt_dubs(pred(b))
}

fun max(x:UInt, y:UInt) {
  if x < y then
    y
  else
    x
}

fun min(x:UInt, y:UInt) {
  if x < y then
    x
  else
    y
}

fun operator *(UInt,UInt) -> UInt

fun operator +(UInt,UInt) -> UInt

fun operator <(UInt,UInt) -> bool

fun operator >(x:UInt, y:UInt) {
  y < x
}

fun operator ^(a:UInt, b:UInt)

fun operator ∸(UInt,UInt) -> UInt

fun operator ≤(x:UInt, y:UInt) {
  (x < y or x = y)
}

fun operator ≥(x:UInt, y:UInt) {
  y ≤ x
}

fun sqr(a:UInt) {
  a * a
}

fun toNat(UInt) -> Nat