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_iff_abs: (all a:Int, b:Int. (divides(a, b) ⇔ divides(abs(a), abs(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_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_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)))
    }