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

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

fromNat_mod: (all x:Nat, y:Nat. fromNat(x) % fromNat(y) = fromNat(x % y))

recfun gcd(a:UInt, b:UInt) -> UInt
measure	b  {
  if b = 0 then
    a
  else
    gcd(b, a % 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
}

toNat_mod: (all x:UInt, y:UInt. toNat(x % y) = toNat(x) % toNat(y))

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

uint_add_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a + b) % m = (a % m + b % m) % m))

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

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

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

uint_div_less: (all n:UInt, m:UInt. (if ((0 < n) and (1 < m)) then n / m < n))

uint_div_less_equal: (all n:UInt, m:UInt. (if 0 < m then n / m ≤ n))

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_div_zero: (all n:UInt. n / 0 = 0)

uint_divides_add: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m + n)))

uint_divides_antisymmetric: (all a:UInt, b:UInt. (if (divides(a, b) and divides(b, a)) then a = b))

uint_divides_less_equal: (all a:UInt, b:UInt. (if (divides(a, b) and (0 < b)) then a ≤ b))

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

uint_divides_mod_of_divides: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m % n)))

uint_divides_monus: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m ∸ n)))

uint_divides_mult_left: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, m * n)))

uint_divides_mult_right: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, n * m)))

uint_divides_refl: (all n:UInt. divides(n, n))

uint_divides_trans: (all a:UInt, b:UInt, c:UInt. (if (divides(a, b) and divides(b, c)) then divides(a, c)))

uint_divides_zero: (all n:UInt. divides(n, 0))

uint_gcd_divides: (all b:UInt, a:UInt. (divides(gcd(a, b), a) and divides(gcd(a, b), b)))

uint_gcd_divides_left: (all a:UInt, b:UInt. divides(gcd(a, b), a))

uint_gcd_divides_right: (all a:UInt, b:UInt. divides(gcd(a, b), b))

uint_gcd_greatest: (all d:UInt, a:UInt, b:UInt. (if (divides(d, a) and divides(d, b)) then divides(d, gcd(a, b))))

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_mod: (all n:UInt, m:UInt. (if 0 < m then (n % m) % m = n % m))

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

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

uint_mod_small: (all n:UInt, m:UInt. (if n < m then n % m = n))

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

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

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

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

uint_mult_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a * b) % m = ((a % m) * (b % m)) % m))

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

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

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

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