define divides : (fn (Int, Int) -> bool) = fun a:Int, b:Int {
      some k:Int. a * k = b
    }

define gcd : (fn (Int, Int) -> Int) = fun a:Int, b:Int {
      pos(gcd(abs(a), abs(b)))
    }

int_divides_add: (all d:Int, m:Int, n:Int. (if (divides(d, m) and divides(d, n)) then divides(d, m + n)))

int_divides_antisymmetric: (all a:Int, b:Int. (if (divides(a, b) and divides(b, a)) then abs(a) = abs(b)))

int_divides_iff_abs: (all a:Int, b:Int. (divides(a, b) ⇔ divides(abs(a), abs(b))))

int_divides_iff_mod_zero: (all m:Int, n:Int. (if m ≠ +0 then (divides(m, n) ⇔ (n % m = +0))))

int_divides_lcm_left: (all a:Int, b:Int. divides(a, lcm(a, b)))

int_divides_lcm_right: (all a:Int, b:Int. divides(b, lcm(a, b)))

int_divides_mult_left: (all d:Int, n:Int, m:Int. (if divides(d, n) then divides(d, m * n)))

int_divides_mult_right: (all d:Int, n:Int, m:Int. (if divides(d, n) then divides(d, n * m)))

int_divides_neg_left: (all d:Int, n:Int. (if divides(d, n) then divides(- d, n)))

int_divides_neg_right: (all d:Int, n:Int. (if divides(d, n) then divides(d, - n)))

int_divides_refl: (all n:Int. divides(n, n))

int_divides_sub: (all d:Int, m:Int, n:Int. (if (divides(d, m) and divides(d, n)) then divides(d, m - n)))

int_divides_trans: (all a:Int, b:Int, c:Int. (if (divides(a, b) and divides(b, c)) then divides(a, c)))

int_divides_zero: (all n:Int. divides(n, +0))

int_gcd_commutative: (all a:Int, b:Int. gcd(a, b) = gcd(b, a))

int_gcd_divides_left: (all a:Int, b:Int. divides(gcd(a, b), a))

int_gcd_divides_right: (all a:Int, b:Int. divides(gcd(a, b), b))

int_gcd_greatest: (all d:Int, a:Int, b:Int. (if (divides(d, a) and divides(d, b)) then divides(d, gcd(a, b))))

int_gcd_lcm_product: (all a:Int, b:Int. gcd(a, b) * lcm(a, b) = pos(abs(a * b)))

int_lcm_commutative: (all a:Int, b:Int. lcm(a, b) = lcm(b, a))

int_lcm_least: (all a:Int, b:Int, m:Int. (if (divides(a, m) and divides(b, m)) then divides(lcm(a, b), m)))

int_lcm_zero_left: (all b:Int. lcm(+0, b) = +0)

int_lcm_zero_right: (all a:Int. lcm(a, +0) = +0)

int_neg_mult_right: (all x:Int, y:Int. x * - y = - (x * y))

int_one_divides: (all n:Int. divides(+1, n))

define lcm : (fn (Int, Int) -> Int) = fun a:Int, b:Int {
      pos(lcm(abs(a), abs(b)))
    }