int_abs_pow: (all n:Int, k:UInt. abs(n ^ k) = abs(n) ^ k)

int_neg_one_pow_even: (all k:UInt. (if Even(k) then - +1 ^ k = +1))

int_neg_one_pow_odd: (all k:UInt. (if Odd(k) then - +1 ^ k = - +1))

auto int_one_pow

int_one_pow: (all k:UInt. +1 ^ k = +1)

int_pow_add: (all n:Int, j:UInt, k:UInt. n ^ (j + k) = n ^ j * n ^ k)

int_pow_eq_zero: (all n:Int, k:UInt. (if n ^ k = +0 then n = +0))

int_pow_mul_base: (all k:UInt, a:Int, b:Int. (a * b) ^ k = a ^ k * b ^ k)

int_pow_mul_exp: (all n:Int, j:UInt, k:UInt. n ^ (j * k) = (n ^ k) ^ j)

int_pow_neg_base_even: (all m:UInt, n:Int. - n ^ (2 * m) = n ^ (2 * m))

int_pow_neg_base_odd: (all m:UInt, n:Int. - n ^ (1 + 2 * m) = - (n ^ (1 + 2 * m)))

int_pow_neg_base_when_even: (all n:Int, k:UInt. (if Even(k) then - n ^ k = n ^ k))

int_pow_neg_base_when_odd: (all n:Int, k:UInt. (if Odd(k) then - n ^ k = - (n ^ k)))

int_pow_nonneg: (all n:Int, k:UInt. (if +0 ≤ n then +0 ≤ n ^ k))

int_pow_nonzero: (all n:Int, k:UInt. (if n ≠ +0 then n ^ k ≠ +0))

auto int_pow_one

int_pow_one: (all n:Int. n ^ 1 = n)

int_pow_one_add: (all n:Int, k:UInt. n ^ (1 + k) = n * n ^ k)

auto int_pow_pos

int_pow_pos: (all m:UInt, k:UInt. pos(m) ^ k = pos(m ^ k))

int_pow_pos_of_pos: (all n:Int, k:UInt. (if +0 < n then +0 < n ^ k))

int_pow_two: (all n:Int. n ^ 2 = n * n)

auto int_pow_zero

int_pow_zero: (all n:Int. n ^ 0 = +1)

int_zero_pow: (all k:UInt. (if 0 < k then +0 ^ k = +0))

opaque define operator ^ : (fn (Int, UInt) -> Int) = fun a:Int, b:UInt {
      expt_nat(toNat(b), a)
    }