union Int {
  pos(Nat)
  negsuc(Nat)
}

fun abs(x:Int) {
  switch x {
    case pos(n) {
      n
    }
    case negsuc(n) {
      suc(n)
    }
  }
}

union Sign {
  positive
  negative
}

fun sign(n:Int) {
  switch n {
    case pos(n') {
      positive
    }
    case negsuc(n') {
      negative
    }
  }
}

fun operator -(x:Int) {
  switch x {
    case pos(n) {
      switch n { case 0 { +0 } case suc(n') { negsuc(n') } }
    }
    case negsuc(n) {
      pos(suc(n))
    }
  }
}

fun operator -(n:Nat) {
  - pos(n)
}

fun operator *(s:Sign, n:Nat) {
  s * pos(n)
}

fun operator ⊝(x:Nat, y:Nat) {
  if x < y then
    - (y - x)
  else
    pos(x - y)
}

fun operator +(x:Int, m:Int) {
  switch x {
    case pos(n) {
      switch m { case pos(n') { pos(n + n') } case negsuc(n') { n ⊝ suc(n') } }
    }
    case negsuc(n) {
      switch m { case pos(n') { n' ⊝ suc(n) } case negsuc(n') { negsuc(suc(n + n')) } }
    }
  }
}

fun operator +(n:Nat, m:Int) {
  pos(n) + m
}

fun operator +(n:Int, m:Nat) {
  n + pos(m)
}

fun operator -(n:Int, m:Int) {
  n + - m
}

fun operator -(n:Nat, m:Int) {
  pos(n) - m
}

fun operator -(n:Int, m:Nat) {
  n - pos(m)
}

fun operator *(x:Int, y:Int) {
  (sign(x) * sign(y)) * (abs(x) * abs(y))
}

fun operator *(n:Nat, m:Int) {
  pos(n) * m
}

fun operator *(n:Int, m:Nat) {
  n * pos(m)
}

fun operator /(n:Int, m:Int) {
  (sign(n) * sign(m)) * (abs(n) / abs(m))
}

fun operator /(n:Int, m:Nat) {
  sign(n) * (abs(n) / m)
}

fun operator ≤(a:Int, y:Int) {
  switch a {
    case pos(x) {
      switch y { case pos(y') { x ≤ y' } case negsuc(y') { false } }
    }
    case negsuc(x) {
      switch y { case pos(y') { true } case negsuc(y') { y' ≤ x } }
    }
  }
}

abs_neg: (all n:Int. abs(- n) = abs(n))

neg_involutive: (all n:Int. - (- n) = n)

int_zero_add: (all n:Int. +0 + n = n)

int_add_zero: (all n:Int. n + +0 = n)

int_add_commute: (all x:Int, y:Int. x + y = y + x)

add_commute_nat_int: (all x:Nat, y:Int. x + y = y + x)

int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))

int_add_inverse: (all x:Int. x + - x = +0)

neg_distr_add: (all x:Int, y:Int. - (x + y) = - x + - y)

int_sub_cancel: (all x:Int. x - x = +0)

int_one_mult: (all x:Int. +1 * x = x)

int_zero_mult: (all x:Int. +0 * x = +0)

int_mult_commute: (all x:Int, y:Int. x * y = y * x)

int_mult_one: (all x:Int. x * +1 = x)

int_mult_zero: (all x:Int. x * +0 = +0)

int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

int_less_equal_refl: (all n:Int. n ≤ n)

int_less_equal_trans: (all m:Int, n:Int, o:Int. (if (m ≤ n and n ≤ o) then m ≤ o))

int_less_equal_antisymmetric: (all x:Int, y:Int. (if (x ≤ y and y ≤ x) then x = y))