int_abs_mod: (all x:Int, y:Int. abs(x % y) = abs(x) % abs(y))

int_div_mod: (all n:Int, m:Int. (if m ≠ +0 then (n / m) * m + n % m = n))

int_div_one: (all n:Int. n / +1 = n)

int_div_self: (all n:Int. (if n ≠ +0 then n / n = +1))

int_div_zero: (all n:Int. n / +0 = +0)

int_mod_less_abs: (all n:Int, m:Int. (if m ≠ +0 then abs(n % m) < abs(m)))

int_mod_neg_divisor: (all n:Int, m:Int. n % - m = n % m)

int_mod_one: (all n:Int. n % +1 = +0)

int_mod_self: (all n:Int. n % n = +0)

int_mod_small: (all n:Int, m:Int. (if abs(n) < abs(m) then n % m = n))

int_mod_zero: (all n:Int. n % +0 = n)

int_zero_div: (all m:Int. +0 / m = +0)

int_zero_mod: (all m:Int. +0 % m = +0)

auto mod_negsuc_negsuc

mod_negsuc_negsuc: (all au:UInt, bu:UInt. negsuc(au) % negsuc(bu) = - pos((1 + au) % (1 + bu)))

auto mod_negsuc_pos

mod_negsuc_pos: (all au:UInt, bu:UInt. negsuc(au) % pos(bu) = - pos((1 + au) % bu))

auto mod_pos_negsuc

mod_pos_negsuc: (all au:UInt, bu:UInt. pos(au) % negsuc(bu) = pos(au % (1 + bu)))

auto mod_pos_pos

mod_pos_pos: (all au:UInt, bu:UInt. pos(au) % pos(bu) = pos(au % bu))

opaque define operator % : (fn (Int, Int) -> Int) = fun n:Int, m:Int {
      sign(n) * (abs(n) % abs(m))
    }