define divides : (fn (UInt, UInt) -> bool) = fun 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 of UInt
{
  if b = 0 then
    a
  else
    gcd(b, a % b)
}
terminates {
  arbitrary a.s26_3 : UInt,
  b.s26_4 : UInt
  assume bnz.s26_5: b ≠ 0
  have b_pos: 0 < b by {
    apply or_not to uint_zero_or_positive[b], bnz
  }
  conclude a % b < b by {
    apply uint_mod_less_divisor[a, b] to b_pos
  }
}

define lcm : (fn (UInt, UInt) -> UInt) = fun a:UInt, b:UInt {
      if ((a = 0) or (b = 0)) then
        0
      else
        (a * b) / gcd(a, b)
    }

define operator % : (fn (UInt, UInt) -> UInt) = fun n:UInt, m:UInt {
      n ∸ (n / m) * m
    }

recfun operator /(n:UInt, m:UInt) -> UInt
  measure n of UInt
{
  if n < m then
    0
  else
    if m = 0 then
      0
    else
      1 + (n ∸ m) / m
}
terminates {
  arbitrary n.s9_3 : UInt,
  m.s9_4 : UInt
  assume cond.s9_5: (not (n < m) and m ≠ 0)
  suffices m + (n ∸ m) < m + n  by {
uint_add_both_sides_of_less[m, n ∸ m, n]
  }
  suffices n < m + n  by {
    have m_n: m ≤ n by {
      apply uint_not_less_implies_less_equal to conjunct 0 of cond
    }
    replace (apply uint_monus_add_identity[n, m] to m_n)
.
  }
  have m_pos: 0 < m by {
    apply uint_not_zero_pos to conjunct 1 of cond
  }
  conclude n < m + n by {
replace uint_add_commute in apply uint_less_add_pos[n, m] to expand lit | fromNat in m_pos
  }
}

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_lcm_left: (all a:UInt, b:UInt. divides(a, lcm(a, b)))

uint_divides_lcm_right: (all a:UInt, b:UInt. divides(b, lcm(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_both: (all k:UInt, a:UInt, b:UInt. (if divides(a, b) then divides(k * a, k * b)))

uint_divides_mult_cancel: (all k:UInt, a:UInt, b:UInt. (if ((0 < k) and divides(k * a, k * b)) then divides(a, b)))

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_commutative: (all a:UInt, b:UInt. gcd(a, b) = gcd(b, a))

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

uint_gcd_lcm_product: (all a:UInt, b:UInt. gcd(a, b) * lcm(a, b) = a * b)

uint_gcd_mult_distributive: (all k:UInt, a:UInt, b:UInt. gcd(k * a, k * b) = k * gcd(a, b))

uint_gcd_pos: (all a:UInt, b:UInt. (if 0 < a then 0 < gcd(a, b)))

uint_gcd_self: (all a:UInt. gcd(a, a) = a)

uint_gcd_zero_left: (all b:UInt. gcd(0, b) = b)

uint_gcd_zero_right: (all a:UInt. gcd(a, 0) = a)

uint_lcm_commutative: (all a:UInt, b:UInt. lcm(a, b) = lcm(b, a))

uint_lcm_least: (all a:UInt, b:UInt, m:UInt. (if (divides(a, m) and divides(b, m)) then divides(lcm(a, b), m)))

auto uint_lcm_zero_left

uint_lcm_zero_left: (all b:UInt. lcm(0, b) = 0)

auto uint_lcm_zero_right

uint_lcm_zero_right: (all a:UInt. lcm(a, 0) = 0)

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)