fun divides(a:UInt, b:UInt) {
  some k:UInt. a * k = b
}

fun operator %(n:UInt, m:UInt) {
  n ∸ (n / m) * m
}

recfun operator /(n:UInt, m:UInt) -> UInt
measure	n  {
  if n < m then
    0
  else
    if m = 0 then
      0
    else
      1 + (n ∸ m) / m
}

uint_add_div_one: (all n:UInt, m:UInt. (if 0 < m then (n + m) / m = 1 + n / m))

uint_div_cancel: (all y:UInt. (if 0 < y then y / y = 1))

uint_div_mod: (all n:UInt, m:UInt. (if 0 < m then (n / m) * m + n % m = n))

uint_div_one: (all n:UInt. n / 1 = n)

uint_divides_mod: (all d:UInt, m:UInt, n:UInt. (if (divides(d, n) and divides(d, m % n) and 0 < n) then divides(d, m)))

auto uint_lit_div

uint_lit_div: (all x:Nat, y:Nat. fromNat(lit(x)) / fromNat(lit(y)) = fromNat(lit(x) / lit(y)))

uint_mod_less_divisor: (all n:UInt, m:UInt. (if 0 < m then n % m < m))

uint_mod_one: (all n:UInt. n % 1 = 0)

uint_mod_self_zero: (all y:UInt. y % y = 0)

uint_mult_div_inverse: (all n:UInt, m:UInt. (if 0 < m then (n * m) / m = n))

uint_zero_div: (all x:UInt. (if 0 < x then 0 / x = 0))

uint_zero_mod: (all x:UInt. 0 % x = 0)