define Even : (fn UInt -> bool) = fun n:UInt {
      some m:UInt. n = 2 * m
    }

define Even : (fn Int -> bool) = fun n:Int {
      some m:Int. n = +2 * m
    }

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

define Odd : (fn UInt -> bool) = fun n:UInt {
      some m:UInt. n = 1 + 2 * m
    }

define Odd : (fn Int -> bool) = fun n:Int {
      some m:Int. n = +1 + +2 * m
    }

opaque union Rat

view UInt {
  source Binary
  target UIntView
  into uint_view
  out uint_unview
  roundtrip uint_view_unview
  inverse uint_unview_view
}

opaque define abs : (fn Int -> UInt)

opaque define abs : (fn Rat -> Rat)

auto abs_lit

abs_lit: (all x:Nat. abs(pos(fromNat(lit(x)))) = fromNat(lit(x)))

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

add_commute_uint_int: (all x:UInt, y:Int. x + y = y + x)

add_pos_pos: (all n:UInt, m:UInt. pos(n) + pos(m) = pos(n + m))

opaque define den : (fn Rat -> UInt)

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

opaque define div2 : (fn UInt -> UInt)

auto div_negsuc_negsuc

div_negsuc_negsuc: (all au:UInt, bu:UInt. negsuc(au) / negsuc(bu) = pos((1 + au) / (1 + bu)))

auto div_negsuc_pos

div_negsuc_pos: (all au:UInt, bu:UInt. negsuc(au) / pos(bu) = - pos((1 + au) / bu))

auto div_negsuc_uint

div_negsuc_uint: (all au:UInt, bu:UInt. negsuc(au) / bu = - pos((1 + au) / bu))

auto div_pos_negsuc

div_pos_negsuc: (all au:UInt, bu:UInt. pos(au) / negsuc(bu) = - pos(au / (1 + bu)))

auto div_pos_pos

div_pos_pos: (all au:UInt, bu:UInt. pos(au) / pos(bu) = pos(au / bu))

auto div_pos_uint

div_pos_uint: (all au:UInt, bu:UInt. pos(au) / bu = pos(au / bu))

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

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

opaque define frac : (fn (Int, UInt) -> Rat)

opaque recursive fromNat(Nat) -> UInt

fromNat_add: (all x:Nat, y:Nat. fromNat(x + y) = fromNat(x) + fromNat(y))

fromNat_div: (all x:Nat, y:Nat. fromNat(x) / fromNat(y) = fromNat(x / y))

fromNat_expt: (all x:Nat, y:Nat. fromNat(x ^ y) = fromNat(x) ^ fromNat(y))

fromNat_injective: (all x:Nat, y:Nat. (if fromNat(x) = fromNat(y) then x = y))

fromNat_mod: (all x:Nat, y:Nat. fromNat(x) % fromNat(y) = fromNat(x % y))

fromNat_mult: (all x:Nat, y:Nat. fromNat(x * y) = fromNat(x) * fromNat(y))

from_one: 1 = 1

from_zero: 0 = 0

recfun gcd(a:UInt, b:UInt) -> UInt
  measure b of UInt
{
  if b = 0 then
    a
  else
    gcd(b, a % b)
}
terminates {
  arbitrary a.s2_s9_s26_3 : UInt,
  b.s2_s9_s26_4 : UInt
  assume bnz.s2_s9_s26_5: b ≠ 0
  have b_pos: 0 < b by {
    apply or_not to uint_zero_or_positive[b], bnz
  }
  conclude a % b < b by {
    apply uint_mod_less_divisor[a, b] to b_pos
  }
}

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

inc_add_one: (all n:UInt. inc(n) = 1 + n)

int_Even_iff_abs_Even: (all x:Int. (Even(x) ⇔ Even(abs(x))))

int_Even_not_Odd: (all n:Int. (Even(n) ⇔ (not Odd(n))))

int_Even_or_Odd: (all n:Int. (Even(n) or Odd(n)))

int_Odd_iff_abs_Odd: (all x:Int. (Odd(x) ⇔ Odd(abs(x))))

int_abs_add: (all x:Int, y:Int. abs(x + y) ≤ abs(x) + abs(y))

int_abs_div: (all x:Int, y:Int. abs(x / y) = abs(x) / abs(y))

int_abs_eq_iff_eq_or_neg: (all x:Int, y:Int. ((abs(x) = abs(y)) ⇔ ((x = y) or (x = - y))))

int_abs_eq_zero_iff_zero: (all x:Int. ((abs(x) = 0) ⇔ (x = +0)))

int_abs_eq_zero_implies_zero: (all x:Int. (if abs(x) = 0 then x = +0))

int_abs_le_iff: (all x:Int, y:UInt. ((abs(x) ≤ y) ⇔ ((- pos(y) ≤ x) and (x ≤ pos(y)))))

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

int_abs_mult: (all x:Int, y:Int. abs(x * y) = abs(x) * abs(y))

auto int_abs_negsuc

int_abs_negsuc: (all n:UInt. abs(negsuc(n)) = 1 + n)

auto int_abs_pos

int_abs_pos: (all n:UInt. abs(pos(n)) = n)

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

int_abs_sub_symm: (all x:Int, y:Int. abs(x - y) = abs(y - x))

auto int_abs_zero

int_abs_zero: abs(+0) = 0

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

int_add_both_sides_of_equal: (all x:Int, y:Int, z:Int. (if x + y = x + z then y = z))

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

int_add_both_sides_of_equal_right: (all x:Int, y:Int, z:Int. (if y + x = z + x then y = z))

int_add_both_sides_of_less: (all x:Int, y:Int, z:Int. ((x + y < x + z) ⇔ (y < z)))

int_add_both_sides_of_less_equal: (all x:Int, y:Int, z:Int. ((x + y ≤ x + z) ⇔ (y ≤ z)))

int_add_both_sides_of_less_equal_right: (all x:Int, y:Int, z:Int. ((y + x ≤ z + x) ⇔ (y ≤ z)))

int_add_both_sides_of_less_right: (all x:Int, y:Int, z:Int. ((y + x < z + x) ⇔ (y < z)))

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

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

int_add_le_left_mono: (all x:Int, y:Int, z:Int. (if y ≤ z then x + y ≤ x + z))

int_add_le_right_mono: (all x:Int, y:Int, z:Int. (if y ≤ z then y + x ≤ z + x))

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

int_add_less_mono_left: (all x:Int, y:Int, z:Int. (if y < z then x + y < x + z))

int_add_less_mono_right: (all x:Int, y:Int, z:Int. (if y < z then y + x < z + x))

int_add_mono_less: (all a:Int, b:Int, c:Int, d:Int. (if ((a < c) and (b < d)) then a + b < c + d))

int_add_mono_less_equal: (all a:Int, b:Int, c:Int, d:Int. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

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

auto int_add_zero

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

int_dichotomy: (all x:Int, y:Int. ((x ≤ y) or (y < x)))

int_dist_mult_add: (all a:Int, x:Int, y:Int. a * (x + y) = a * x + a * y)

int_dist_mult_add_right: (all a:Int, x:Int, y:Int. (x + y) * a = x * a + y * a)

int_dist_mult_sub: (all a:Int, x:Int, y:Int. a * (x - y) = a * x - a * 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_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_even_add_even: (all x:Int, y:Int. (if (Even(x) and Even(y)) then Even(x + y)))

int_even_add_odd: (all x:Int, y:Int. (if (Even(x) and Odd(y)) then Odd(x + y)))

int_even_mult_left: (all x:Int, y:Int. (if Even(x) then Even(x * y)))

int_even_mult_right: (all x:Int, y:Int. (if Even(y) then Even(x * y)))

int_even_neg: (all x:Int. (Even(x) ⇔ Even(- x)))

int_even_one_odd: (all n:Int. (if Even(+1 + n) then Odd(n)))

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_greater_implies_not_equal: (all x:Int, y:Int. (if x > y then x ≠ y))

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_le_abs: (all x:Int. x ≤ pos(abs(x)))

int_le_iff_diff_nonneg: (all a:Int, b:Int. ((a ≤ b) ⇔ (+0 ≤ b - a)))

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

int_less_equal_iff_less_or_equal: (all x:Int, y:Int. ((x ≤ y) ⇔ ((x < y) or (x = y))))

int_less_equal_iff_not_greater: (all x:Int, y:Int. ((x ≤ y) ⇔ (not (y < x))))

int_less_equal_implies_less_or_equal: (all x:Int, y:Int. (if x ≤ y then ((x < y) or (x = y))))

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_iff_diff_pos: (all a:Int, b:Int. ((a < b) ⇔ (+0 < b - a)))

int_less_implies_less_equal: (all x:Int, y:Int. (if x < y then x ≤ y))

int_less_implies_not_equal: (all x:Int, y:Int. (if x < y then x ≠ y))

int_less_implies_not_greater: (all x:Int, y:Int. (if x < y then not (y < x)))

int_less_irreflexive: (all x:Int. not (x < x))

int_less_or_equal_implies_less_equal: (all x:Int, y:Int. (if ((x < y) or (x = y)) then x ≤ y))

int_less_trans: (all x:Int, y:Int, z:Int. (if ((x < y) and (y < z)) then x < z))

int_less_trans_less_equal_left: (all x:Int, y:Int, z:Int. (if ((x ≤ y) and (y < z)) then x < z))

int_less_trans_less_equal_right: (all x:Int, y:Int, z:Int. (if ((x < y) and (y ≤ z)) then x < z))

auto int_lit_negsuc_eq

int_lit_negsuc_eq: (all x:Nat, y:Nat. (negsuc(fromNat(lit(x))) = negsuc(fromNat(lit(y)))) = (fromNat(lit(x)) = fromNat(lit(y))))

auto int_lit_pos_eq

int_lit_pos_eq: (all x:Nat, y:Nat. (pos(fromNat(lit(x))) = pos(fromNat(lit(y)))) = (fromNat(lit(x)) = fromNat(lit(y))))

auto int_lit_sub_negsuc_negsuc

int_lit_sub_negsuc_negsuc: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) - negsuc(fromNat(lit(y))) = negsuc(fromNat(lit(x))) + - negsuc(fromNat(lit(y))))

auto int_lit_sub_negsuc_pos

int_lit_sub_negsuc_pos: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) - pos(fromNat(lit(y))) = negsuc(fromNat(lit(x))) + - pos(fromNat(lit(y))))

auto int_lit_sub_pos_negsuc

int_lit_sub_pos_negsuc: (all x:Nat, y:Nat. pos(fromNat(lit(x))) - negsuc(fromNat(lit(y))) = pos(fromNat(lit(x))) + - negsuc(fromNat(lit(y))))

auto int_lit_sub_pos_pos

int_lit_sub_pos_pos: (all x:Nat, y:Nat. pos(fromNat(lit(x))) - pos(fromNat(lit(y))) = pos(fromNat(lit(x))) + - pos(fromNat(lit(y))))

int_max_assoc: (all x:Int, y:Int, z:Int. max(max(x, y), z) = max(x, max(y, z)))

int_max_equal_greater_left: (all x:Int, y:Int. (if y ≤ x then max(x, y) = x))

int_max_equal_greater_right: (all x:Int, y:Int. (if x ≤ y then max(x, y) = y))

int_max_greater_left: (all x:Int, y:Int. x ≤ max(x, y))

int_max_greater_right: (all x:Int, y:Int. y ≤ max(x, y))

int_max_idempotent: (all x:Int. max(x, x) = x)

int_max_is_left_or_right: (all x:Int, y:Int. ((max(x, y) = x) or (max(x, y) = y)))

int_max_less_equal: (all x:Int, y:Int, z:Int. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

int_max_min_absorb_left: (all x:Int, y:Int. max(x, min(x, y)) = x)

int_max_min_absorb_right: (all x:Int, y:Int. max(min(x, y), x) = x)

int_max_symmetric: (all x:Int, y:Int. max(x, y) = max(y, x))

int_min_assoc: (all x:Int, y:Int, z:Int. min(min(x, y), z) = min(x, min(y, z)))

int_min_equal_less_left: (all x:Int, y:Int. (if x ≤ y then min(x, y) = x))

int_min_equal_less_right: (all x:Int, y:Int. (if y ≤ x then min(x, y) = y))

int_min_greatest_less_equal: (all x:Int, y:Int, z:Int. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

int_min_idempotent: (all x:Int. min(x, x) = x)

int_min_is_left_or_right: (all x:Int, y:Int. ((min(x, y) = x) or (min(x, y) = y)))

int_min_less_equal_left: (all x:Int, y:Int. min(x, y) ≤ x)

int_min_less_equal_right: (all x:Int, y:Int. min(x, y) ≤ y)

int_min_max_absorb_left: (all x:Int, y:Int. min(x, max(x, y)) = x)

int_min_max_absorb_right: (all x:Int, y:Int. min(max(x, y), x) = x)

int_min_symmetric: (all x:Int, y:Int. min(x, y) = min(y, x))

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_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

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

int_mult_left_cancel: (all n:Int, x:Int, y:Int. (if (n ≠ +0 and (n * x = n * y)) then x = y))

auto int_mult_one

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

int_mult_right_cancel: (all n:Int, x:Int, y:Int. (if (n ≠ +0 and (x * n = y * n)) then x = y))

int_mult_to_zero: (all x:Int, y:Int. (if x * y = +0 then ((x = +0) or (y = +0))))

auto int_mult_zero

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

int_neg_abs_le: (all x:Int. - pos(abs(x)) ≤ x)

int_neg_injective: (all x:Int, y:Int. (if - x = - y then x = y))

int_neg_le_iff: (all x:Int, y:Int. ((x ≤ y) ⇔ (- y ≤ - x)))

int_neg_le_mono: (all x:Int, y:Int. (if x ≤ y then - y ≤ - x))

int_neg_less_iff: (all x:Int, y:Int. ((x < y) ⇔ (- y < - x)))

int_neg_less_mono: (all x:Int, y:Int. (if x < y then - y < - x))

int_neg_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x ≤ n * y)) then y ≤ x))

int_neg_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x < n * y)) then y < x))

int_neg_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then n * y < n * x))

int_neg_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then y * n < x * n))

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

int_neg_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n ≤ y * n)) then y ≤ x))

int_neg_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n < y * n)) then y < x))

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))

int_negsuc_eq_pos_false: (all x:UInt, y:UInt. negsuc(x) ≠ pos(y))

int_negsuc_injective: (all x:UInt, y:UInt. (if negsuc(x) = negsuc(y) then x = y))

auto int_negsuc_le_negsuc

int_negsuc_le_negsuc: (all au:UInt, bu:UInt. (negsuc(au) ≤ negsuc(bu)) = (bu ≤ au))

auto int_negsuc_le_pos

int_negsuc_le_pos: (all au:UInt, bu:UInt. (negsuc(au) ≤ pos(bu)) = true)

auto int_negsuc_less_negsuc

int_negsuc_less_negsuc: (all au:UInt, bu:UInt. (negsuc(au) < negsuc(bu)) = (bu < au))

auto int_negsuc_less_pos

int_negsuc_less_pos: (all au:UInt, bu:UInt. (negsuc(au) < pos(bu)) = true)

int_nonneg_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then n * x ≤ n * y))

int_nonneg_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then x * n ≤ y * n))

int_nonpos_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then n * y ≤ n * x))

int_nonpos_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then y * n ≤ x * n))

int_not_less_equal_iff_greater: (all x:Int, y:Int. ((not (x ≤ y)) ⇔ (y < x)))

int_not_less_implies_less_equal: (all x:Int, y:Int. (if not (x < y) then y ≤ x))

int_odd_add_even: (all x:Int, y:Int. (if (Odd(x) and Even(y)) then Odd(x + y)))

int_odd_add_odd: (all x:Int, y:Int. (if (Odd(x) and Odd(y)) then Even(x + y)))

int_odd_mult_odd: (all x:Int, y:Int. (if (Odd(x) and Odd(y)) then Odd(x * y)))

int_odd_neg: (all x:Int. (Odd(x) ⇔ Odd(- x)))

int_odd_one_even: (all n:Int. (if Odd(+1 + n) then Even(n)))

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

auto int_one_mult

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

auto int_one_pow

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

int_one_two_odd: (all n:Int. Odd(+1 + +2 * n))

int_pos_abs_eq_iff_nonneg: (all x:Int. ((pos(abs(x)) = x) ⇔ (+0 ≤ x)))

int_pos_eq_negsuc_false: (all x:UInt, y:UInt. pos(x) ≠ negsuc(y))

int_pos_injective: (all x:UInt, y:UInt. (if pos(x) = pos(y) then x = y))

auto int_pos_le_negsuc

int_pos_le_negsuc: (all au:UInt, bu:UInt. (pos(au) ≤ negsuc(bu)) = false)

auto int_pos_le_pos

int_pos_le_pos: (all au:UInt, bu:UInt. (pos(au) ≤ pos(bu)) = (au ≤ bu))

auto int_pos_less_negsuc

int_pos_less_negsuc: (all au:UInt, bu:UInt. (pos(au) < negsuc(bu)) = false)

auto int_pos_less_pos

int_pos_less_pos: (all au:UInt, bu:UInt. (pos(au) < pos(bu)) = (au < bu))

int_pos_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x ≤ n * y)) then x ≤ y))

int_pos_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x < n * y)) then x < y))

int_pos_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then n * x < n * y))

int_pos_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then x * n < y * n))

int_pos_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n ≤ y * n)) then x ≤ y))

int_pos_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n < y * n)) then x < y))

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:UInt) = 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:UInt) = n * n)

auto int_pow_zero

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

int_rev_triangle: (all x:Int, y:Int. abs(x) ∸ abs(y) ≤ abs(x - y))

int_rev_triangle_right: (all x:Int, y:Int. abs(y) ∸ abs(x) ≤ abs(x - y))

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

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

define int_summation : (fn (UInt, UInt, (fn UInt -> Int)) -> Int) = fun k:UInt, begin:UInt, f:(fn UInt -> Int) {
      int_summation_nat(toNat(k), toNat(begin), f)
    }

int_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int), h:(fn UInt -> Int). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then int_summation(a + b, s, f) = int_summation(a, s, g) + int_summation(b, t, h))))

int_summation_add_pointwise: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) + g(i) }) = int_summation(k, s, f) + int_summation(k, s, g))

int_summation_cong: (all k:UInt. (all f:(fn UInt -> Int), g:(fn UInt -> Int), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then int_summation(k, s, f) = int_summation(k, t, g))))

int_summation_const_zero: (all k:UInt, s:UInt. int_summation(k, s, fun i:UInt { +0 }) = +0)

recursive int_summation_nat(Nat,Nat,(fn UInt -> Int)) -> Int{
  int_summation_nat(zero, begin, f) = +0
  int_summation_nat(suc(k), begin, f) = f(fromNat(begin)) + int_summation_nat(k, suc(begin), f)
}

int_summation_neg: (all k:UInt, s:UInt, f:(fn UInt -> Int). int_summation(k, s, fun i:UInt { - f(i) }) = - int_summation(k, s, f))

int_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> Int). int_summation(1 + n, s, f) = int_summation(n, s, f) + f(s + n))

int_summation_sub: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) - g(i) }) = int_summation(k, s, f) - int_summation(k, s, g))

int_summation_zero: (all begin:UInt, f:(fn UInt -> Int). int_summation(0, begin, f) = +0)

int_trichotomy: (all x:Int, y:Int. ((x < y) or (x = y) or (y < x)))

int_two_even: (all n:Int. Even(+2 * n))

auto int_zero_add

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

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

int_zero_implies_abs_eq_zero: (all x:Int. (if x = +0 then abs(x) = 0))

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

auto int_zero_mult

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

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

opaque define inv : (fn Rat -> Rat)

define lcm : (fn (UInt, UInt) -> UInt) = fun a:UInt, b:UInt {
      if ((a = 0) or (b = 0)) then
        0
      else
        (a * b) / gcd(a, b)
    }

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

less_equal_fromNat: (all x:Nat, y:Nat. (if x ≤ y then fromNat(x) ≤ fromNat(y)))

less_equal_toNat: (all x:UInt, y:UInt. (if toNat(x) ≤ toNat(y) then x ≤ y))

less_fromNat: (all x:Nat, y:Nat. (if x < y then fromNat(x) < fromNat(y)))

less_pow_log: (all n:UInt. (if 0 < n then n < 2 ^ (1 + log(n))))

less_toNat: (all x:UInt, y:UInt. (if toNat(x) < toNat(y) then x < y))

auto lit_add_fromNat

lit_add_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) + fromNat(lit(y)) = fromNat(lit(x) + lit(y)))

auto lit_add_lit_pos

lit_add_lit_pos: (all x:Nat, y:Nat. fromNat(lit(x)) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_negsuc_negsuc

lit_add_negsuc_negsuc: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) + negsuc(fromNat(lit(y))) = negsuc((1 + fromNat(lit(x))) + fromNat(lit(y))))

auto lit_add_negsuc_pos_suc

lit_add_negsuc_pos_suc: (all x:Nat, y:Nat. negsuc(fromNat(lit(suc(x)))) + pos(fromNat(lit(suc(y)))) = negsuc(fromNat(lit(x))) + pos(fromNat(lit(y))))

auto lit_add_negsuc_zero_pos_suc

lit_add_negsuc_zero_pos_suc: (all x:Nat, y:Nat. -1 + pos(fromNat(lit(suc(y)))) = pos(fromNat(lit(y))))

auto lit_add_pos_lit

lit_add_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + fromNat(lit(y)) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_pos_negsuc_suc

lit_add_pos_negsuc_suc: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(suc(x)))) = pos(fromNat(lit(y))) + negsuc(fromNat(lit(x))))

auto lit_add_pos_pos

lit_add_pos_pos: (all x:Nat, y:Nat. pos(fromNat(lit(x))) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y))))

auto lit_add_pos_suc_negsuc_zero

lit_add_pos_suc_negsuc_zero: (all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + -1 = pos(fromNat(lit(y))))

auto lit_expt_fromNat

lit_expt_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ^ fromNat(lit(y)) = fromNat(lit(x) ^ lit(y)))

auto lit_monus_fromNat

lit_monus_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) ∸ fromNat(lit(y)) = fromNat(lit(x) ∸ lit(y)))

auto lit_mult_fromNat

lit_mult_fromNat: (all x:Nat, y:Nat. fromNat(lit(x)) * fromNat(lit(y)) = fromNat(lit(x) * lit(y)))

auto lit_pow_mul_r

lit_pow_mul_r: (all m:Nat, n:Nat, o:UInt. fromNat(lit(m)) ^ (fromNat(lit(n)) * o) = (fromNat(lit(m)) ^ fromNat(lit(n))) ^ o)

opaque define log : (fn UInt -> UInt)

log_pow: (all n:UInt. log(2 ^ n) = n)

define max : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        y
      else
        x
    }

define max : (fn (Int, Int) -> Int) = fun x:Int, y:Int {
      if x < y then
        y
      else
        x
    }

define max : (fn (Rat, Rat) -> Rat) = fun x:Rat, y:Rat {
      if x < y then
        y
      else
        x
    }

define min : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        x
      else
        y
    }

define min : (fn (Int, Int) -> Int) = fun x:Int, y:Int {
      if x < y then
        x
      else
        y
    }

define min : (fn (Rat, Rat) -> Rat) = fun x:Rat, y:Rat {
      if x < y then
        x
      else
        y
    }

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))

auto mult_lit_neg_lit

mult_lit_neg_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))

auto mult_lit_pos_lit

mult_lit_pos_lit: (all x:Nat, y:Nat. fromNat(lit(x)) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))

auto mult_neg_lit_lit

mult_neg_lit_lit: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * fromNat(lit(y)) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))

auto mult_neg_lit_neg_lit

mult_neg_lit_neg_lit: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * negsuc(fromNat(lit(y))) = pos((1 + fromNat(lit(x))) * (1 + fromNat(lit(y)))))

auto mult_neg_lit_pos

mult_neg_lit_pos: (all x:Nat, y:Nat. negsuc(fromNat(lit(x))) * pos(fromNat(lit(y))) = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x))))

auto mult_pos_lit_lit

mult_pos_lit_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * fromNat(lit(y)) = pos(fromNat(lit(x) * lit(y))))

auto mult_pos_lit_neg_lit

mult_pos_lit_neg_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * negsuc(fromNat(lit(y))) = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y))))

auto mult_pos_lit_pos_lit

mult_pos_lit_pos_lit: (all x:Nat, y:Nat. pos(fromNat(lit(x))) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y))))

mult_pos_pos: (all x:UInt, y:UInt. pos(x) * pos(y) = pos(x * y))

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

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

auto neg_lit_suc

neg_lit_suc: (all x:Nat. - fromNat(lit(suc(x))) = negsuc(fromNat(lit(x))))

auto neg_lit_zero

neg_lit_zero: - +0 = +0

auto neg_negsuc_lit

neg_negsuc_lit: (all x:Nat. - negsuc(fromNat(lit(x))) = pos(fromNat(lit(suc(x)))))

neg_pos: (all n:UInt. - pos(1 + n) = negsuc(n))

auto neg_pos_lit_suc

neg_pos_lit_suc: (all x:Nat. - pos(fromNat(lit(suc(x)))) = negsuc(fromNat(lit(x))))

auto neg_uint_zero

neg_uint_zero: - 0 = +0

neg_zero: - +0 = +0

opaque define num : (fn Rat -> Int)

define operator % : (fn (UInt, UInt) -> UInt) = fun n:UInt, m:UInt {
      n ∸ (n / m) * m
    }

opaque define operator % : (fn (Int, Int) -> Int)

opaque recursive operator *(UInt,UInt) -> UInt

opaque define operator * : (fn (Int, Int) -> Int)

opaque define operator * : (fn (UInt, Int) -> Int)

opaque define operator * : (fn (Int, UInt) -> Int)

opaque define operator * : (fn (Rat, Rat) -> Rat)

opaque recursive operator +(UInt,UInt) -> UInt

opaque define operator + : (fn (Int, Int) -> Int)

opaque define operator + : (fn (UInt, Int) -> Int)

opaque define operator + : (fn (Int, UInt) -> Int)

opaque define operator + : (fn (Rat, Rat) -> Rat)

opaque define operator - : (fn Int -> Int)

opaque define operator - : (fn UInt -> Int)

define operator - : (fn (Int, Int) -> Int) = fun n:Int, m:Int {
      n + - m
    }

opaque define operator - : (fn (UInt, Int) -> Int)

opaque define operator - : (fn (Int, UInt) -> Int)

opaque define operator - : (fn (UInt, UInt) -> Int)

opaque define operator - : (fn Rat -> Rat)

opaque define operator - : (fn (Rat, Rat) -> Rat)

recfun operator /(n:UInt, m:UInt) -> UInt
  measure n of UInt
{
  if n < m then
    0
  else
    if m = 0 then
      0
    else
      1 + (n ∸ m) / m
}
terminates {
  arbitrary n.s2_s9_s9_3 : UInt,
  m.s2_s9_s9_4 : UInt
  assume cond.s2_s9_s9_5: (not (n < m) and m ≠ 0)
  suffices m + (n ∸ m) < m + n  by {
uint_add_both_sides_of_less[m, n ∸ m, n]
  }
  suffices n < m + n  by {
    have m_n: m ≤ n by {
      apply uint_not_less_implies_less_equal to conjunct 0 of cond
    }
    replace (apply uint_monus_add_identity[n, m] to m_n)
.
  }
  have m_pos: 0 < m by {
    apply uint_not_zero_pos to conjunct 1 of cond
  }
  conclude n < m + n by {
replace uint_add_commute in apply uint_less_add_pos[n, m] to expand lit | fromNat in m_pos
  }
}

opaque define operator / : (fn (Int, Int) -> Int)

opaque define operator / : (fn (Int, UInt) -> Int)

opaque define operator / : (fn (Rat, Rat) -> Rat)

opaque recursive operator <(UInt,UInt) -> bool

opaque define operator < : (fn (Int, Int) -> bool)

opaque define operator < : (fn (Rat, Rat) -> bool)

define operator > : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y < x
    }

define operator > : (fn (Int, Int) -> bool) = fun x:Int, y:Int {
      y < x
    }

define operator > : (fn (Rat, Rat) -> bool) = fun x:Rat, y:Rat {
      y < x
    }

opaque define operator ^ : (fn (UInt, UInt) -> UInt)

opaque define operator ^ : (fn (Int, UInt) -> Int)

opaque recursive operator ∸(UInt,UInt) -> UInt

define operator ≤ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      ((x < y) or (x = y))
    }

opaque define operator ≤ : (fn (Int, Int) -> bool)

opaque define operator ≤ : (fn (Rat, Rat) -> bool)

define operator ≥ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y ≤ x
    }

define operator ≥ : (fn (Int, Int) -> bool) = fun x:Int, y:Int {
      y ≤ x
    }

define operator ≥ : (fn (Rat, Rat) -> bool) = fun x:Rat, y:Rat {
      y ≤ x
    }

opaque define rat : (fn Int -> Rat)

opaque define rat : (fn UInt -> Rat)

rat_abs_add: (all x:Rat, y:Rat. abs(x + y) ≤ abs(x) + abs(y))

rat_abs_le_iff: (all x:Rat, y:Rat. (abs(x) ≤ y) = ((- y ≤ x) and (x ≤ y)))

rat_abs_mult: (all x:Rat, y:Rat. abs(x * y) = abs(x) * abs(y))

rat_abs_neg: (all x:Rat. abs(- x) = abs(x))

rat_abs_nonneg: (all x:Rat. rat(+0) ≤ abs(x))

rat_abs_nonneg_eq: (all x:Rat. (if rat(+0) ≤ x then abs(x) = x))

rat_abs_nonpos_eq: (all x:Rat. (if x ≤ rat(+0) then abs(x) = - x))

rat_add_assoc: (all x:Rat, y:Rat, z:Rat. (x + y) + z = x + (y + z))

rat_add_both_sides_of_equal: (all x:Rat, y:Rat, z:Rat. (x + y = x + z) = (y = z))

rat_add_both_sides_of_equal_right: (all x:Rat, y:Rat, z:Rat. (y + x = z + x) = (y = z))

rat_add_both_sides_of_less: (all x:Rat, y:Rat, z:Rat. (x + y < x + z) = (y < z))

rat_add_both_sides_of_less_equal: (all x:Rat, y:Rat, z:Rat. (x + y ≤ x + z) = (y ≤ z))

rat_add_both_sides_of_less_equal_right: (all x:Rat, y:Rat, z:Rat. (y + x ≤ z + x) = (y ≤ z))

rat_add_both_sides_of_less_right: (all x:Rat, y:Rat, z:Rat. (y + x < z + x) = (y < z))

rat_add_commute: (all x:Rat, y:Rat. x + y = y + x)

rat_add_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then frac(n, d) + frac(m, e) = frac(n * pos(e) + m * pos(d), d * e)))

rat_add_inverse: (all x:Rat. x + - x = rat(+0))

rat_add_left_inverse: (all x:Rat. - x + x = rat(+0))

rat_add_mono_less: (all a:Rat, b:Rat, c:Rat, d:Rat. (if ((a < c) and (b < d)) then a + b < c + d))

rat_add_mono_less_equal: (all a:Rat, b:Rat, c:Rat, d:Rat. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

rat_add_sub_cancel: (all x:Rat, y:Rat. (x + y) - y = x)

auto rat_add_zero

rat_add_zero: (all x:Rat. x + rat(+0) = x)

rat_den_int: (all n:Int. den(rat(n)) = 1)

rat_den_neg: (all x:Rat. den(- x) = den(x))

rat_den_pos: (all x:Rat. 0 < den(x))

rat_dichotomy: (all x:Rat, y:Rat. ((x ≤ y) or (y < x)))

rat_dist_mult_add: (all x:Rat, y:Rat, z:Rat. x * (y + z) = x * y + x * z)

rat_dist_mult_add_right: (all x:Rat, y:Rat, z:Rat. (y + z) * x = y * x + z * x)

rat_dist_mult_sub: (all x:Rat, y:Rat, z:Rat. x * (y - z) = x * y - x * z)

rat_dist_mult_sub_right: (all x:Rat, y:Rat, z:Rat. (y - z) * x = y * x - z * x)

rat_div_def: (all x:Rat, y:Rat. x / y = x * inv(y))

rat_div_mult_cancel: (all x:Rat, y:Rat. (if y ≠ rat(+0) then (x / y) * y = x))

auto rat_div_one

rat_div_one: (all x:Rat. x / rat(+1) = x)

rat_div_self: (all x:Rat. (if x ≠ rat(+0) then x / x = rat(+1)))

auto rat_div_zero

rat_div_zero: (all x:Rat. x / rat(+0) = rat(+0))

rat_eq_cross: (all x:Rat, y:Rat. (if num(x) * pos(den(y)) = num(y) * pos(den(x)) then x = y))

rat_frac_cross: (all n:Int, d:UInt. (if 0 < d then num(frac(n, d)) * pos(d) = n * pos(den(frac(n, d)))))

rat_frac_cross_eq: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e) and (n * pos(e) = m * pos(d))) then frac(n, d) = frac(m, e)))

rat_frac_div: (all n:Int, d:UInt. frac(n, d) = rat(n) / rat(pos(d)))

rat_frac_eq_cross: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e) and (frac(n, d) = frac(m, e))) then n * pos(e) = m * pos(d)))

rat_frac_eq_iff: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) = frac(m, e)) = (n * pos(e) = m * pos(d))))

auto rat_frac_lit_add

rat_frac_lit_add: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) + frac(m, fromNat(lit(suc(z)))) = frac(n * pos(fromNat(lit(suc(z)))) + m * pos(fromNat(lit(suc(y)))), fromNat(lit(suc(y))) * fromNat(lit(suc(z)))))

auto rat_frac_lit_add_int

rat_frac_lit_add_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) + rat(m) = frac(n + m * pos(fromNat(lit(suc(y)))), fromNat(lit(suc(y))) * 1))

auto rat_frac_lit_div

rat_frac_lit_div: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) / frac(m, fromNat(lit(suc(z)))) = frac(n, fromNat(lit(suc(y)))) * inv(frac(m, fromNat(lit(suc(z))))))

auto rat_frac_lit_div_int

rat_frac_lit_div_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) / rat(m) = frac(n, fromNat(lit(suc(y)))) * inv(rat(m)))

auto rat_frac_lit_eq

rat_frac_lit_eq: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) = frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) = m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_eq_int

rat_frac_lit_eq_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) = rat(m)) = (n = m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_le

rat_frac_lit_le: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) ≤ frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) ≤ m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_le_int

rat_frac_lit_le_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) ≤ rat(m)) = (n ≤ m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_less

rat_frac_lit_less: (all n:Int, y:Nat, m:Int, z:Nat. (frac(n, fromNat(lit(suc(y)))) < frac(m, fromNat(lit(suc(z))))) = (n * pos(fromNat(lit(suc(z)))) < m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_less_int

rat_frac_lit_less_int: (all n:Int, y:Nat, m:Int. (frac(n, fromNat(lit(suc(y)))) < rat(m)) = (n < m * pos(fromNat(lit(suc(y))))))

auto rat_frac_lit_mult

rat_frac_lit_mult: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) * frac(m, fromNat(lit(suc(z)))) = frac(n * m, fromNat(lit(suc(y))) * fromNat(lit(suc(z)))))

auto rat_frac_lit_mult_int

rat_frac_lit_mult_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) * rat(m) = frac(n * m, fromNat(lit(suc(y))) * 1))

auto rat_frac_lit_neg

rat_frac_lit_neg: (all n:Int, y:Nat. - frac(n, fromNat(lit(suc(y)))) = frac(- n, fromNat(lit(suc(y)))))

auto rat_frac_lit_one

rat_frac_lit_one: (all n:Int. frac(n, 1) = rat(n))

auto rat_frac_lit_reduce

rat_frac_lit_reduce: (all x:Nat, y:Nat. (if 1 < gcd(fromNat(lit(suc(x))), fromNat(lit(suc(y)))) then frac(pos(fromNat(lit(suc(x)))), fromNat(lit(suc(y)))) = frac(pos(fromNat(lit(suc(x)) / gcd(lit(suc(x)), lit(suc(y))))), fromNat(lit(suc(y)) / gcd(lit(suc(x)), lit(suc(y)))))))

auto rat_frac_lit_reduce_neg

rat_frac_lit_reduce_neg: (all x:Nat, y:Nat. (if 1 < gcd(fromNat(lit(suc(x))), fromNat(lit(suc(y)))) then frac(negsuc(fromNat(lit(x))), fromNat(lit(suc(y)))) = frac(- pos(fromNat(lit(suc(x)) / gcd(lit(suc(x)), lit(suc(y))))), fromNat(lit(suc(y)) / gcd(lit(suc(x)), lit(suc(y)))))))

auto rat_frac_lit_sub

rat_frac_lit_sub: (all n:Int, y:Nat, m:Int, z:Nat. frac(n, fromNat(lit(suc(y)))) - frac(m, fromNat(lit(suc(z)))) = frac(n, fromNat(lit(suc(y)))) + frac(- m, fromNat(lit(suc(z)))))

auto rat_frac_lit_sub_int

rat_frac_lit_sub_int: (all n:Int, y:Nat, m:Int. frac(n, fromNat(lit(suc(y)))) - rat(m) = frac(n, fromNat(lit(suc(y)))) + rat(- m))

auto rat_frac_lit_zero

rat_frac_lit_zero: (all n:Int. frac(n, 0) = rat(+0))

rat_frac_neg: (all n:Int, d:UInt. frac(- n, d) = - frac(n, d))

rat_frac_num_den: (all x:Rat. frac(num(x), den(x)) = x)

rat_frac_rep: (all x:Rat. some n:Int,d:UInt. ((0 < d) and (x = frac(n, d))))

rat_frac_scale: (all k:UInt, n:Int, d:UInt. (if 0 < k then frac(pos(k) * n, k * d) = frac(n, d)))

rat_frac_self: (all k:UInt. (if 0 < k then frac(pos(k), k) = rat(+1)))

auto rat_frac_zero

rat_frac_zero: (all d:UInt. frac(+0, d) = rat(+0))

auto rat_int_add

rat_int_add: (all n:Int, m:Int. rat(n) + rat(m) = rat(n + m))

auto rat_int_add_frac_lit

rat_int_add_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) + frac(n, fromNat(lit(suc(y)))) = frac(m * pos(fromNat(lit(suc(y)))) + n, 1 * fromNat(lit(suc(y)))))

auto rat_int_div

rat_int_div: (all n:Int, m:Int. rat(n) / rat(m) = rat(n) * inv(rat(m)))

auto rat_int_div_frac_lit

rat_int_div_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) / frac(n, fromNat(lit(suc(y)))) = rat(m) * inv(frac(n, fromNat(lit(suc(y))))))

auto rat_int_eq

rat_int_eq: (all n:Int, m:Int. (rat(n) = rat(m)) = (n = m))

auto rat_int_eq_frac_lit

rat_int_eq_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) = frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) = n))

rat_int_frac: (all n:Int. rat(n) = frac(n, 1))

rat_int_injective: (all n:Int, m:Int. (if rat(n) = rat(m) then n = m))

auto rat_int_le

rat_int_le: (all n:Int, m:Int. (rat(n) ≤ rat(m)) = (n ≤ m))

auto rat_int_le_frac_lit

rat_int_le_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) ≤ frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) ≤ n))

auto rat_int_less

rat_int_less: (all n:Int, m:Int. (rat(n) < rat(m)) = (n < m))

auto rat_int_less_frac_lit

rat_int_less_frac_lit: (all m:Int, n:Int, y:Nat. (rat(m) < frac(n, fromNat(lit(suc(y))))) = (m * pos(fromNat(lit(suc(y)))) < n))

auto rat_int_mult

rat_int_mult: (all n:Int, m:Int. rat(n) * rat(m) = rat(n * m))

auto rat_int_mult_frac_lit

rat_int_mult_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) * frac(n, fromNat(lit(suc(y)))) = frac(m * n, 1 * fromNat(lit(suc(y)))))

auto rat_int_neg

rat_int_neg: (all n:Int. - rat(n) = rat(- n))

auto rat_int_sub

rat_int_sub: (all n:Int, m:Int. rat(n) - rat(m) = rat(n - m))

auto rat_int_sub_frac_lit

rat_int_sub_frac_lit: (all m:Int, n:Int, y:Nat. rat(m) - frac(n, fromNat(lit(suc(y)))) = rat(m) + frac(- n, fromNat(lit(suc(y)))))

rat_inv_frac: (all a:UInt, d:UInt. (if ((0 < a) and (0 < d)) then inv(frac(pos(a), d)) = frac(pos(d), a)))

auto rat_inv_frac_lit_neg

rat_inv_frac_lit_neg: (all x:Nat, y:Nat. inv(frac(negsuc(fromNat(lit(x))), fromNat(lit(suc(y))))) = frac(- pos(fromNat(lit(suc(y)))), fromNat(lit(suc(x)))))

auto rat_inv_frac_lit_pos

rat_inv_frac_lit_pos: (all x:Nat, y:Nat. inv(frac(pos(fromNat(lit(suc(x)))), fromNat(lit(suc(y))))) = frac(pos(fromNat(lit(suc(y)))), fromNat(lit(suc(x)))))

rat_inv_frac_neg: (all a:UInt, d:UInt. (if ((0 < a) and (0 < d)) then inv(frac(- pos(a), d)) = frac(- pos(d), a)))

auto rat_inv_int_lit_neg

rat_inv_int_lit_neg: (all x:Nat. inv(rat(negsuc(fromNat(lit(x))))) = frac(- 1, fromNat(lit(suc(x)))))

auto rat_inv_int_lit_pos

rat_inv_int_lit_pos: (all x:Nat. inv(rat(pos(fromNat(lit(suc(x)))))) = frac(+1, fromNat(lit(suc(x)))))

rat_inv_inv: (all x:Rat. inv(inv(x)) = x)

rat_inv_mult: (all x:Rat. (if x ≠ rat(+0) then inv(x) * x = rat(+1)))

rat_inv_mult_distr: (all x:Rat, y:Rat. inv(x * y) = inv(x) * inv(y))

rat_inv_neg: (all x:Rat. inv(- x) = - inv(x))

rat_inv_one: inv(rat(+1)) = rat(+1)

rat_inv_pos: (all x:Rat. (if rat(+0) < x then rat(+0) < inv(x)))

rat_inv_unique: (all x:Rat, y:Rat. (if x * y = rat(+1) then inv(x) = y))

auto rat_inv_zero

rat_inv_zero: inv(rat(+0)) = rat(+0)

rat_le_abs: (all x:Rat. x ≤ abs(x))

rat_le_def: (all x:Rat, y:Rat. (x ≤ y) = (num(x) * pos(den(y)) ≤ num(y) * pos(den(x))))

rat_le_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) ≤ frac(m, e)) = (n * pos(e) ≤ m * pos(d))))

rat_le_iff_sub_nonneg: (all x:Rat, y:Rat. (x ≤ y) = (rat(+0) ≤ y - x))

rat_le_zero_num: (all x:Rat. (x ≤ rat(+0)) = (num(x) ≤ +0))

rat_less_def: (all x:Rat, y:Rat. (x < y) = (num(x) * pos(den(y)) < num(y) * pos(den(x))))

rat_less_equal_antisymmetric: (all x:Rat, y:Rat. (if ((x ≤ y) and (y ≤ x)) then x = y))

rat_less_equal_iff_less_or_equal: (all x:Rat, y:Rat. ((x ≤ y) ⇔ ((x < y) or (x = y))))

rat_less_equal_iff_not_greater: (all x:Rat, y:Rat. ((x ≤ y) ⇔ (not (y < x))))

rat_less_equal_refl: (all x:Rat. x ≤ x)

rat_less_equal_trans: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ y) and (y ≤ z)) then x ≤ z))

rat_less_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then (frac(n, d) < frac(m, e)) = (n * pos(e) < m * pos(d))))

rat_less_iff_sub_pos: (all x:Rat, y:Rat. (x < y) = (rat(+0) < y - x))

rat_less_implies_less_equal: (all x:Rat, y:Rat. (if x < y then x ≤ y))

rat_less_implies_not_equal: (all x:Rat, y:Rat. (if x < y then x ≠ y))

rat_less_implies_not_greater: (all x:Rat, y:Rat. (if x < y then not (y < x)))

rat_less_irreflexive: (all x:Rat. not (x < x))

rat_less_trans: (all x:Rat, y:Rat, z:Rat. (if ((x < y) and (y < z)) then x < z))

rat_less_trans_less_equal_left: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ y) and (y < z)) then x < z))

rat_less_trans_less_equal_right: (all x:Rat, y:Rat, z:Rat. (if ((x < y) and (y ≤ z)) then x < z))

rat_less_zero_num: (all x:Rat. (x < rat(+0)) = (num(x) < +0))

rat_max_equal_greater_left: (all x:Rat, y:Rat. (if y ≤ x then max(x, y) = x))

rat_max_equal_greater_right: (all x:Rat, y:Rat. (if x ≤ y then max(x, y) = y))

rat_max_greater_left: (all x:Rat, y:Rat. x ≤ max(x, y))

rat_max_greater_right: (all x:Rat, y:Rat. y ≤ max(x, y))

rat_max_less_equal: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

rat_max_symmetric: (all x:Rat, y:Rat. max(x, y) = max(y, x))

rat_min_equal_less_left: (all x:Rat, y:Rat. (if x ≤ y then min(x, y) = x))

rat_min_equal_less_right: (all x:Rat, y:Rat. (if y ≤ x then min(x, y) = y))

rat_min_greatest_less_equal: (all x:Rat, y:Rat, z:Rat. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

rat_min_less_equal_left: (all x:Rat, y:Rat. min(x, y) ≤ x)

rat_min_less_equal_right: (all x:Rat, y:Rat. min(x, y) ≤ y)

rat_min_symmetric: (all x:Rat, y:Rat. min(x, y) = min(y, x))

rat_mult_assoc: (all x:Rat, y:Rat, z:Rat. (x * y) * z = x * (y * z))

rat_mult_commute: (all x:Rat, y:Rat. x * y = y * x)

rat_mult_div_cancel: (all x:Rat, y:Rat. (if y ≠ rat(+0) then (x * y) / y = x))

rat_mult_frac: (all n:Int, d:UInt, m:Int, e:UInt. (if ((0 < d) and (0 < e)) then frac(n, d) * frac(m, e) = frac(n * m, d * e)))

rat_mult_inv: (all x:Rat. (if x ≠ rat(+0) then x * inv(x) = rat(+1)))

rat_mult_left_cancel: (all x:Rat, y:Rat, z:Rat. (if (x ≠ rat(+0) and (x * y = x * z)) then y = z))

rat_mult_neg: (all x:Rat, y:Rat. x * - y = - (x * y))

rat_mult_nonneg: (all x:Rat, y:Rat. (if ((rat(+0) ≤ x) and (rat(+0) ≤ y)) then rat(+0) ≤ x * y))

auto rat_mult_one

rat_mult_one: (all x:Rat. x * rat(+1) = x)

rat_mult_pos: (all x:Rat, y:Rat. (if ((rat(+0) < x) and (rat(+0) < y)) then rat(+0) < x * y))

rat_mult_right_cancel: (all x:Rat, y:Rat, z:Rat. (if (x ≠ rat(+0) and (y * x = z * x)) then y = z))

rat_mult_to_zero: (all x:Rat, y:Rat. (if x * y = rat(+0) then ((x = rat(+0)) or (y = rat(+0)))))

auto rat_mult_zero

rat_mult_zero: (all x:Rat. x * rat(+0) = rat(+0))

rat_neg_abs_le: (all x:Rat. - abs(x) ≤ x)

rat_neg_distr_add: (all x:Rat, y:Rat. - (x + y) = - x + - y)

rat_neg_injective: (all x:Rat, y:Rat. (if - x = - y then x = y))

rat_neg_involutive: (all x:Rat. - (- x) = x)

rat_neg_le_iff: (all x:Rat, y:Rat. (- y ≤ - x) = (x ≤ y))

rat_neg_less_iff: (all x:Rat, y:Rat. (- y < - x) = (x < y))

rat_neg_mult: (all x:Rat, y:Rat. - x * y = - (x * y))

rat_neg_mult_neg: (all x:Rat, y:Rat. - x * - y = x * y)

rat_neg_one_mult: (all x:Rat. - rat(+1) * x = - x)

rat_neg_sub: (all x:Rat, y:Rat. - (x - y) = y - x)

auto rat_neg_zero

rat_neg_zero: - rat(+0) = rat(+0)

rat_nonneg_mult_mono_le_left: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) ≤ z) and (x ≤ y)) then z * x ≤ z * y))

rat_nonneg_mult_mono_le_right: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) ≤ z) and (x ≤ y)) then x * z ≤ y * z))

rat_not_less_equal_iff_greater: (all x:Rat, y:Rat. ((not (x ≤ y)) ⇔ (y < x)))

rat_not_less_implies_less_equal: (all x:Rat, y:Rat. (if not (x < y) then y ≤ x))

rat_num_int: (all n:Int. num(rat(n)) = n)

rat_num_neg: (all x:Rat. num(- x) = - num(x))

auto rat_one_mult

rat_one_mult: (all x:Rat. rat(+1) * x = x)

rat_one_not_zero: rat(+1) ≠ rat(+0)

rat_pos_mult_le_iff: (all z:Rat, x:Rat, y:Rat. (if rat(+0) < z then (x * z ≤ y * z) = (x ≤ y)))

rat_pos_mult_less_iff: (all z:Rat, x:Rat, y:Rat. (if rat(+0) < z then (x * z < y * z) = (x < y)))

rat_pos_mult_mono_less_left: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) < z) and (x < y)) then z * x < z * y))

rat_pos_mult_mono_less_right: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) < z) and (x < y)) then x * z < y * z))

rat_square_nonneg: (all x:Rat. rat(+0) ≤ x * x)

rat_sub_add_cancel: (all x:Rat, y:Rat. (x - y) + y = x)

auto rat_sub_cancel

rat_sub_cancel: (all x:Rat. x - x = rat(+0))

rat_sub_def: (all x:Rat, y:Rat. x - y = x + - y)

rat_sub_eq_zero_iff: (all x:Rat, y:Rat. (x - y = rat(+0)) = (x = y))

auto rat_sub_zero

rat_sub_zero: (all x:Rat. x - rat(+0) = x)

rat_trichotomy: (all x:Rat, y:Rat. ((x < y) or (x = y) or (y < x)))

rat_uint_int: (all n:UInt. rat(n) = rat(pos(n)))

auto rat_zero_add

rat_zero_add: (all x:Rat. rat(+0) + x = x)

auto rat_zero_div

rat_zero_div: (all x:Rat. rat(+0) / x = rat(+0))

rat_zero_le_frac: (all n:Int, d:UInt. (if 0 < d then (rat(+0) ≤ frac(n, d)) = (+0 ≤ n)))

rat_zero_le_neg: (all x:Rat. (rat(+0) ≤ - x) = (x ≤ rat(+0)))

rat_zero_le_num: (all x:Rat. (rat(+0) ≤ x) = (+0 ≤ num(x)))

rat_zero_less_frac: (all n:Int, d:UInt. (if 0 < d then (rat(+0) < frac(n, d)) = (+0 < n)))

rat_zero_less_neg: (all x:Rat. (rat(+0) < - x) = (x < rat(+0)))

rat_zero_less_num: (all x:Rat. (rat(+0) < x) = (+0 < num(x)))

rat_zero_less_one: rat(+0) < rat(+1)

auto rat_zero_mult

rat_zero_mult: (all x:Rat. rat(+0) * x = rat(+0))

auto rat_zero_sub

rat_zero_sub: (all x:Rat. rat(+0) - x = - x)

auto sign_neg_lit

sign_neg_lit: (all x:Nat. sign(negsuc(fromNat(lit(x)))) = negative)

auto sign_pos_lit

sign_pos_lit: (all x:Nat. sign(pos(fromNat(lit(x)))) = positive)

define sqr : (fn UInt -> UInt) = fun a:UInt {
      a * a
    }

suc_uint_monuso: (all x:UInt, y:UInt. (1 + x) ⊝ (1 + y) = x ⊝ y)

opaque recursive toNat(UInt) -> Nat

toNat_add: (all x:UInt, y:UInt. toNat(x + y) = toNat(x) + toNat(y))

toNat_expt: (all p:UInt, n:UInt. toNat(n ^ p) = toNat(n) ^ toNat(p))

toNat_less: (all x:UInt, y:UInt. (if x < y then toNat(x) < toNat(y)))

toNat_less_equal: (all x:UInt, y:UInt. (if x ≤ y then toNat(x) ≤ toNat(y)))

toNat_mod: (all x:UInt, y:UInt. toNat(x % y) = toNat(x) % toNat(y))

toNat_monus: (all x:UInt, y:UInt. toNat(x ∸ y) = toNat(x) ∸ toNat(y))

toNat_mult: (all x:UInt, y:UInt. toNat(x * y) = toNat(x) * toNat(y))

toNat_uint_summation: (all k:UInt, begin:UInt, f:(fn UInt -> UInt). toNat(uint_summation(k, begin, f)) = summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))

uint_Even_not_Odd: (all n:UInt. (Even(n) ⇔ (not Odd(n))))

uint_Even_or_Odd: (all n:UInt. (Even(n) or Odd(n)))

uint_add_assoc: (all x:UInt, y:UInt, z:UInt. (x + y) + z = x + (y + z))

uint_add_both_monus: (all z:UInt, y:UInt, x:UInt. (z + y) ∸ (z + x) = y ∸ x)

uint_add_both_sides_of_equal: (all x:UInt, y:UInt, z:UInt. ((x + y = x + z) ⇔ (y = z)))

auto uint_add_both_sides_of_le_equal

uint_add_both_sides_of_le_equal: (all x:UInt. (all y:UInt, z:UInt. (x + y ≤ x + z) = (y ≤ z)))

uint_add_both_sides_of_less: (all x:UInt, y:UInt, z:UInt. ((x + y < x + z) ⇔ (y < z)))

uint_add_both_sides_of_less_equal: (all x:UInt. (all y:UInt, z:UInt. ((x + y ≤ x + z) ⇔ (y ≤ z))))

uint_add_commute: (all x:UInt, y:UInt. x + y = y + x)

uint_add_div_one: (all n:UInt, m:UInt. (if 0 < m then (n + m) / m = 1 + n / m))

uint_add_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a + b) % m = (a % m + b % m) % m))

uint_add_mono_less: (all a:UInt, b:UInt, c:UInt, d:UInt. (if ((a < c) and (b < d)) then a + b < c + d))

uint_add_mono_less_equal: (all a:UInt, b:UInt, c:UInt, d:UInt. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

auto uint_add_monus_identity

uint_add_monus_identity: (all m:UInt, n:UInt. (m + n) ∸ m = n)

uint_add_mult_div: (all n:UInt, k:UInt, m:UInt. (if 0 < m then (n + k * m) / m = k + n / m))

uint_add_mult_mod: (all n:UInt, k:UInt, m:UInt. (if 0 < m then (n + k * m) % m = n % m))

uint_add_one_le_double: (all x:UInt. (if 0 < x then 1 + x ≤ x + x))

uint_add_to_zero: (all n:UInt, m:UInt. (if n + m = 0 then ((n = 0) and (m = 0))))

auto uint_add_zero

uint_add_zero: (all x:UInt. x + 0 = x)

uint_dichotomy: (all x:UInt, y:UInt. ((x ≤ y) or (y < x)))

uint_dist_mult_add: (all a:UInt, x:UInt, y:UInt. a * (x + y) = a * x + a * y)

uint_dist_mult_add_right: (all x:UInt, y:UInt, a:UInt. (x + y) * a = x * a + y * a)

uint_dist_mult_monus: (all x:UInt. (all y:UInt, z:UInt. x * (y ∸ z) = x * y ∸ x * z))

uint_div_cancel: (all y:UInt. (if 0 < y then y / y = 1))

uint_div_less: (all n:UInt, m:UInt. (if ((0 < n) and (1 < m)) then n / m < n))

uint_div_less_equal: (all n:UInt, m:UInt. (if 0 < m then n / m ≤ n))

uint_div_mod: (all n:UInt, m:UInt. (if 0 < m then (n / m) * m + n % m = n))

uint_div_one: (all n:UInt. n / 1 = n)

uint_div_zero: (all n:UInt. n / 0 = 0)

uint_divides_add: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m + n)))

uint_divides_antisymmetric: (all a:UInt, b:UInt. (if (divides(a, b) and divides(b, a)) then a = b))

uint_divides_lcm_left: (all a:UInt, b:UInt. divides(a, lcm(a, b)))

uint_divides_lcm_right: (all a:UInt, b:UInt. divides(b, lcm(a, b)))

uint_divides_less_equal: (all a:UInt, b:UInt. (if (divides(a, b) and (0 < b)) then a ≤ b))

uint_divides_mod: (all d:UInt, m:UInt, n:UInt. (if (divides(d, n) and divides(d, m % n) and (0 < n)) then divides(d, m)))

uint_divides_mod_of_divides: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m % n)))

uint_divides_monus: (all d:UInt, m:UInt, n:UInt. (if (divides(d, m) and divides(d, n)) then divides(d, m ∸ n)))

uint_divides_mult_both: (all k:UInt, a:UInt, b:UInt. (if divides(a, b) then divides(k * a, k * b)))

uint_divides_mult_cancel: (all k:UInt, a:UInt, b:UInt. (if ((0 < k) and divides(k * a, k * b)) then divides(a, b)))

uint_divides_mult_left: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, m * n)))

uint_divides_mult_right: (all d:UInt, n:UInt, m:UInt. (if divides(d, n) then divides(d, n * m)))

uint_divides_refl: (all n:UInt. divides(n, n))

uint_divides_trans: (all a:UInt, b:UInt, c:UInt. (if (divides(a, b) and divides(b, c)) then divides(a, c)))

uint_divides_zero: (all n:UInt. divides(n, 0))

auto uint_equal

uint_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) = fromNat(lit(y))) = (x = y))

uint_equal_implies_less_equal: (all x:UInt, y:UInt. (if x = y then x ≤ y))

uint_even_add_even: (all x:UInt, y:UInt. (if (Even(x) and Even(y)) then Even(x + y)))

uint_even_add_odd: (all x:UInt, y:UInt. (if (Even(x) and Odd(y)) then Odd(x + y)))

uint_even_mult_left: (all x:UInt, y:UInt. (if Even(x) then Even(x * y)))

uint_even_mult_right: (all x:UInt, y:UInt. (if Even(y) then Even(x * y)))

uint_even_one_odd: (all n:UInt. (if Even(1 + n) then Odd(n)))

uint_expt_log_less_equal: (all n:UInt. (if 0 < n then 2 ^ log(n) ≤ n))

uint_expt_one: (all n:UInt. n ^ 1 = n)

auto uint_expt_suc

uint_expt_suc: (all n:UInt, m:Nat. n ^ fromNat(lit(suc(m))) = n * n ^ fromNat(lit(m)))

uint_expt_two: (all n:UInt. n ^ 2 = n * n)

auto uint_expt_zero

uint_expt_zero: (all n:UInt. n ^ 0 = 1)

uint_fromNat_toNat: (all b:UInt. fromNat(toNat(b)) = b)

uint_gcd_commutative: (all a:UInt, b:UInt. gcd(a, b) = gcd(b, a))

uint_gcd_divides: (all b:UInt, a:UInt. (divides(gcd(a, b), a) and divides(gcd(a, b), b)))

uint_gcd_divides_left: (all a:UInt, b:UInt. divides(gcd(a, b), a))

uint_gcd_divides_right: (all a:UInt, b:UInt. divides(gcd(a, b), b))

uint_gcd_greatest: (all d:UInt, a:UInt, b:UInt. (if (divides(d, a) and divides(d, b)) then divides(d, gcd(a, b))))

uint_gcd_lcm_product: (all a:UInt, b:UInt. gcd(a, b) * lcm(a, b) = a * b)

uint_gcd_mult_distributive: (all k:UInt, a:UInt, b:UInt. gcd(k * a, k * b) = k * gcd(a, b))

uint_gcd_pos: (all a:UInt, b:UInt. (if 0 < a then 0 < gcd(a, b)))

uint_gcd_self: (all a:UInt. gcd(a, a) = a)

uint_gcd_zero_left: (all b:UInt. gcd(0, b) = b)

uint_gcd_zero_right: (all a:UInt. gcd(a, 0) = a)

uint_greater_implies_not_equal: (all x:UInt, y:UInt. (if x > y then x ≠ y))

uint_induction: (all P:(fn UInt -> bool). (if (P(0) and (all m:UInt. (if P(m) then P(1 + m)))) then (all n:UInt. P(n))))

uint_k_induction: (all P:(fn UInt -> bool), k:UInt. (if (P(k) and (all m:UInt. (if ((k ≤ m) and P(m)) then P(1 + m)))) then (all n:UInt. (if k ≤ n then P(n)))))

uint_lcm_commutative: (all a:UInt, b:UInt. lcm(a, b) = lcm(b, a))

uint_lcm_least: (all a:UInt, b:UInt, m:UInt. (if (divides(a, m) and divides(b, m)) then divides(lcm(a, b), m)))

auto uint_lcm_zero_left

uint_lcm_zero_left: (all b:UInt. lcm(0, b) = 0)

auto uint_lcm_zero_right

uint_lcm_zero_right: (all a:UInt. lcm(a, 0) = 0)

uint_le_exists_monus: (all n:UInt, m:UInt. (if n ≤ m then some x:UInt. m = n + x))

uint_less_add_one_implies_less_equal: (all x:UInt, y:UInt. (if x < 1 + y then x ≤ y))

uint_less_equal_add: (all x:UInt, y:UInt. x ≤ x + y)

uint_less_equal_add_left: (all x:UInt, y:UInt. y ≤ x + y)

uint_less_equal_antisymmetric: (all x:UInt, y:UInt. (if ((x ≤ y) and (y ≤ x)) then x = y))

uint_less_equal_refl: (all n:UInt. n ≤ n)

auto uint_less_equal_refl_true

uint_less_equal_refl_true: (all n:UInt. (n ≤ n) = true)

uint_less_equal_trans: (all x:UInt, y:UInt, z:UInt. (if ((x ≤ y) and (y ≤ z)) then x ≤ z))

uint_less_equal_zero: (all x:UInt. (if x ≤ 0 then x = 0))

uint_less_implies_less_equal: (all x:UInt, y:UInt. (if x < y then x ≤ y))

uint_less_implies_not_equal: (all x:UInt, y:UInt. (if x < y then x ≠ y))

uint_less_implies_not_greater: (all x:UInt, y:UInt. (if x < y then not (y < x)))

uint_less_irreflexive: (all x:UInt. not (x < x))

uint_less_is_less_equal: (all x:UInt, y:UInt. (x < y) = (1 + x ≤ y))

uint_less_plus1: (all n:UInt. n < 1 + n)

auto uint_less_plus1_true

uint_less_plus1_true: (all n:UInt. (n < 1 + n) = true)

auto uint_less_refl_false

uint_less_refl_false: (all x:UInt. (x < x) = false)

uint_less_trans: (all x:UInt, y:UInt, z:UInt. (if ((x < y) and (y < z)) then x < z))

auto uint_lit_div

uint_lit_div: (all x:Nat, y:Nat. fromNat(lit(x)) / fromNat(lit(y)) = fromNat(lit(x) / lit(y)))

auto uint_lit_less

uint_lit_less: (all x:Nat, y:Nat. (fromNat(lit(x)) < fromNat(lit(y))) = (lit(x) < lit(y)))

auto uint_lit_less_equal

uint_lit_less_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) ≤ fromNat(lit(y))) = (lit(x) ≤ lit(y)))

uint_log_add_le_log_mult: (all m:UInt, n:UInt. (if ((0 < m) and (0 < n)) then log(m) + log(n) ≤ log(m * n)))

uint_log_greater_one: (all n:UInt. (if 2 ≤ n then 1 ≤ log(n)))

uint_log_lt: (all n:UInt, m:UInt. (if 0 < n then ((log(n) < m) ⇔ (n < 2 ^ m))))

uint_log_mono: (all x:UInt, y:UInt. (if x ≤ y then log(x) ≤ log(y)))

uint_log_mult_le_log_add: (all m:UInt, n:UInt. log(m * n) ≤ (1 + log(m)) + log(n))

auto uint_log_one

uint_log_one: log(1:UInt) = 0

uint_log_pos: (all n:UInt. (if 1 < n then 0 < log(n)))

uint_log_two: log(2:UInt) = 1

auto uint_log_zero

uint_log_zero: log(0:UInt) = 0

uint_logn_le_n: (all n:UInt. log(n) ≤ n)

uint_max_assoc: (all x:UInt, y:UInt, z:UInt. max(max(x, y), z) = max(x, max(y, z)))

uint_max_equal_greater_left: (all x:UInt, y:UInt. (if y ≤ x then max(x, y) = x))

uint_max_equal_greater_right: (all x:UInt, y:UInt. (if x ≤ y then max(x, y) = y))

uint_max_greater_left: (all x:UInt, y:UInt. x ≤ max(x, y))

uint_max_greater_right: (all x:UInt, y:UInt. y ≤ max(x, y))

uint_max_idempotent: (all x:UInt. max(x, x) = x)

uint_max_is_left_or_right: (all x:UInt, y:UInt. ((max(x, y) = x) or (max(x, y) = y)))

uint_max_less_equal: (all x:UInt, y:UInt, z:UInt. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

uint_max_min_absorb_left: (all x:UInt, y:UInt. max(x, min(x, y)) = x)

uint_max_min_absorb_right: (all x:UInt, y:UInt. max(min(x, y), x) = x)

uint_max_symmetric: (all x:UInt, y:UInt. max(x, y) = max(y, x))

auto uint_max_zero

uint_max_zero: (all x:UInt. max(x, 0) = x)

uint_min_equal_less_left: (all x:UInt, y:UInt. (if x ≤ y then min(x, y) = x))

uint_min_equal_less_right: (all x:UInt, y:UInt. (if y ≤ x then min(x, y) = y))

uint_min_greatest_less_equal: (all x:UInt, y:UInt, z:UInt. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

uint_min_idempotent: (all x:UInt. min(x, x) = x)

uint_min_is_left_or_right: (all x:UInt, y:UInt. ((min(x, y) = x) or (min(x, y) = y)))

uint_min_less_equal_left: (all x:UInt, y:UInt. min(x, y) ≤ x)

uint_min_less_equal_right: (all x:UInt, y:UInt. min(x, y) ≤ y)

uint_min_max_absorb_left: (all x:UInt, y:UInt. min(x, max(x, y)) = x)

uint_min_max_absorb_right: (all x:UInt, y:UInt. min(max(x, y), x) = x)

uint_min_symmetric: (all x:UInt, y:UInt. min(x, y) = min(y, x))

uint_mod_less_divisor: (all n:UInt, m:UInt. (if 0 < m then n % m < m))

uint_mod_mod: (all n:UInt, m:UInt. (if 0 < m then (n % m) % m = n % m))

uint_mod_one: (all n:UInt. n % 1 = 0)

uint_mod_self_zero: (all y:UInt. y % y = 0)

uint_mod_small: (all n:UInt, m:UInt. (if n < m then n % m = n))

uint_monus_add_assoc: (all n:UInt, l:UInt, m:UInt. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m))

uint_monus_add_identity: (all n:UInt. (all m:UInt. (if m ≤ n then m + (n ∸ m) = n)))

auto uint_monus_cancel

uint_monus_cancel: (all n:UInt. n ∸ n = 0)

uint_monus_monus_eq_monus_add: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = x ∸ (y + z))

uint_monus_one_less: (all n:UInt. (if n ≠ 0 then n ∸ 1 < n))

uint_monus_order: (all x:UInt, y:UInt, z:UInt. (x ∸ y) ∸ z = (x ∸ z) ∸ y)

auto uint_monus_zero

uint_monus_zero: (all n:UInt. n ∸ 0 = n)

uint_monus_zero_iff_less_eq: (all x:UInt, y:UInt. ((x ≤ y) ⇔ (x ∸ y = 0)))

uint_mult_add_div: (all k:UInt, n:UInt, m:UInt. (if 0 < m then (k * m + n) / m = k + n / m))

uint_mult_add_mod: (all k:UInt, n:UInt, m:UInt. (if 0 < m then (k * m + n) % m = n % m))

uint_mult_assoc: (all m:UInt, n:UInt, o:UInt. (m * n) * o = m * (n * o))

uint_mult_commute: (all m:UInt, n:UInt. m * n = n * m)

uint_mult_div_inverse: (all n:UInt, m:UInt. (if 0 < m then (n * m) / m = n))

uint_mult_div_left_inverse: (all n:UInt, m:UInt. (if 0 < m then (m * n) / m = n))

uint_mult_mod: (all a:UInt, b:UInt, m:UInt. (if 0 < m then (a * b) % m = ((a % m) * (b % m)) % m))

uint_mult_mod_left_zero: (all n:UInt, m:UInt. (if 0 < m then (m * n) % m = 0))

uint_mult_mod_right_zero: (all n:UInt, m:UInt. (if 0 < m then (n * m) % m = 0))

uint_mult_mono_le: (all n:UInt, x:UInt, y:UInt. (if x ≤ y then n * x ≤ n * y))

uint_mult_mono_le2: (all n:UInt, x:UInt, m:UInt, y:UInt. (if ((n ≤ m) and (x ≤ y)) then n * x ≤ m * y))

auto uint_mult_one

uint_mult_one: (all n:UInt. n * 1 = n)

uint_mult_to_zero: (all n:UInt, m:UInt. (if n * m = 0 then ((n = 0) or (m = 0))))

auto uint_mult_zero

uint_mult_zero: (all n:UInt. n * 0 = 0)

uint_not_less_equal_iff_greater: (all x:UInt, y:UInt. ((not (x ≤ y)) ⇔ (y < x)))

uint_not_less_implies_less_equal: (all x:UInt, y:UInt. (if not (x < y) then y ≤ x))

uint_not_less_zero: (all x:UInt. not (x < 0))

uint_not_one_add_le_zero: (all n:UInt. not (1 + n ≤ 0))

uint_not_one_add_zero: (all n:UInt. 1 + n ≠ 0)

uint_not_zero_pos: (all n:UInt. (if n ≠ 0 then 0 < n))

uint_odd_add_even: (all x:UInt, y:UInt. (if (Odd(x) and Even(y)) then Odd(x + y)))

uint_odd_add_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Even(x + y)))

uint_odd_mult_odd: (all x:UInt, y:UInt. (if (Odd(x) and Odd(y)) then Odd(x * y)))

uint_odd_one_even: (all n:UInt. (if Odd(1 + n) then Even(n)))

auto uint_one_add_zero_false

uint_one_add_zero_false: (all n:UInt. (1 + n = 0) = false)

auto uint_one_expt

uint_one_expt: (all n:UInt. 1 ^ n = 1)

auto uint_one_mult

uint_one_mult: (all n:UInt. 1 * n = n)

uint_one_two_odd: (all n:UInt. Odd(1 + 2 * n))

uint_pos_implies_one_le: (all n:UInt. (if 0 < n then 1 ≤ n))

uint_pos_mult_both_sides_of_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x < y)) then n * x < n * y))

uint_pos_mult_left_cancel: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x = n * y)) then x = y))

uint_pos_mult_left_cancel_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x < n * y)) then x < y))

uint_pos_mult_left_cancel_less_equal: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (n * x ≤ n * y)) then x ≤ y))

uint_pos_mult_right_cancel: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n = y * n)) then x = y))

uint_pos_mult_right_cancel_less: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n < y * n)) then x < y))

uint_pos_mult_right_cancel_less_equal: (all n:UInt, x:UInt, y:UInt. (if ((0 < n) and (x * n ≤ y * n)) then x ≤ y))

uint_pos_not_zero: (all n:UInt. (if 0 < n then n ≠ 0))

uint_positive_add_one: (all n:UInt. (if 0 < n then some n':UInt. n = 1 + n'))

uint_pow_add_r: (all m:UInt, n:UInt, o:UInt. m ^ (n + o) = m ^ n * m ^ o)

uint_pow_eq_one: (all m:UInt, n:UInt. (if m ^ n = 1 then ((n = 0) or (m = 1))))

uint_pow_eq_zero: (all m:UInt, n:UInt. (if m ^ n = 0 then m = 0))

uint_pow_gt_one: (all n:UInt, m:UInt. (if 1 < n then ((0 < m) ⇔ (1 < n ^ m))))

uint_pow_inj_l: (all a:UInt, b:UInt, c:UInt. (if 0 < c then (if a ^ c = b ^ c then a = b)))

uint_pow_inj_r: (all a:UInt, b:UInt, c:UInt. (if 1 < a then (if a ^ b = a ^ c then b = c)))

uint_pow_le_mono_l: (all c:UInt, a:UInt, b:UInt. (if a ≤ b then a ^ c ≤ b ^ c))

uint_pow_le_mono_r: (all c:UInt, a:UInt, b:UInt. (if 1 ≤ a then (if b ≤ c then a ^ b ≤ a ^ c)))

uint_pow_lt_implies_lt: (all c:UInt, a:UInt, b:UInt. (if 0 < c then (if a ^ c < b ^ c then a < b)))

uint_pow_lt_mono_l: (all c:UInt, a:UInt, b:UInt. (if 0 < c then (if a < b then a ^ c < b ^ c)))

uint_pow_lt_mono_r: (all c:UInt, a:UInt, b:UInt. (if 1 < a then (if b < c then a ^ b < a ^ c)))

uint_pow_mul_l: (all m:UInt, n:UInt, o:UInt. (m * n) ^ o = m ^ o * n ^ o)

uint_pow_mul_r: (all m:UInt, n:UInt, o:UInt. (m ^ n) ^ o = m ^ (n * o))

uint_pow_pos: (all a:UInt, b:UInt. (if 0 < a then 0 < a ^ b))

uint_strong_induction: (all P:(fn UInt -> bool), n:UInt. (if (all j:UInt. (if (all i:UInt. (if i < j then P(i))) then P(j))) then P(n)))

define uint_summation : (fn (UInt, UInt, (fn UInt -> UInt)) -> UInt) = fun k:UInt, begin:UInt, f:(fn UInt -> UInt) {
      fromNat(summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))
    }

uint_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then uint_summation(a + b, s, f) = uint_summation(a, s, g) + uint_summation(b, t, h))))

uint_summation_cong: (all k:UInt. (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then uint_summation(k, s, f) = uint_summation(k, t, g))))

uint_summation_const_one: (all n:UInt. (all s:UInt. uint_summation(n, s, fun i:UInt { 1 }) = n))

uint_summation_id: (all n:UInt. 2 * uint_summation(n, 0, fun i:UInt { i }) = n * (n ∸ 1))

uint_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> UInt). uint_summation(1 + n, s, f) = uint_summation(n, s, f) + f(s + n))

uint_summation_pow2_succ: (all n:UInt. (1:UInt) + uint_summation(n, 0, fun i:UInt { 2 ^ i }) = 2 ^ n)

uint_summation_pow_succ: (all a:UInt. (if 1 ≤ a then (all n:UInt. (1:UInt) + (a ∸ 1) * uint_summation(n, 0, fun i:UInt { a ^ i }) = a ^ n)))

uint_toNat_fromNat: (all x:Nat. toNat(fromNat(x)) = x)

uint_toNat_injective: (all x:UInt, y:UInt. (if toNat(x) = toNat(y) then x = y))

uint_trichotomy: (all x:UInt, y:UInt. ((x < y) or (x = y) or (y < x)))

uint_two_even: (all n:UInt. Even(2 * n))

uint_two_mult: (all n:UInt. 2 * n = n + n)

auto uint_zero_add

uint_zero_add: (all x:UInt. 0 + x = x)

uint_zero_div: (all x:UInt. (if 0 < x then 0 / x = 0))

uint_zero_le: (all x:UInt. 0 ≤ x)

uint_zero_le_zero: (all x:UInt. (if x ≤ 0 then x = 0))

auto uint_zero_less_equal_true

uint_zero_less_equal_true: (all x:UInt. (0 ≤ x) = true)

uint_zero_less_one_add: (all n:UInt. 0 < 1 + n)

auto uint_zero_less_one_add_true

uint_zero_less_one_add_true: (all n:UInt. (0 < 1 + n) = true)

auto uint_zero_max

uint_zero_max: (all x:UInt. max(0, x) = x)

uint_zero_mod: (all x:UInt. 0 % x = 0)

auto uint_zero_mult

uint_zero_mult: (all n:UInt. 0 * n = 0)

uint_zero_or_add_one: (all x:UInt. ((x = 0) or some x':UInt. x = 1 + x'))

uint_zero_or_positive: (all x:UInt. ((x = 0) or (0 < x)))

uint_zero_pow: (all a:UInt. (if 0 < a then (0:UInt) ^ a = 0))