module UInt

import Base
import Nat
import UIntDefs
import UIntToFrom
import UIntLess
import UIntAdd
import UIntMonus
import UIntMult

/*
  UInt division, modulo, and divisibility.

  Division and modulo are defined by repeated subtraction over UInt.
  The proofs below establish their Nat correspondence, divisor
  bounds, inverse facts, and divisibility lemmas.
*/

// Quotient by repeated subtraction, returning zero for division by zero.
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:UInt, m:UInt
  assume cond: not (n < m) and not (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
  }
}

// Remainder after removing the quotient times the divisor.
fun operator % (n:UInt, m:UInt) {
  n ∸ (n / m) * m
}

// Dividing zero by a positive UInt yields zero.
theorem uint_zero_div: all x:UInt. if 0 < x then 0 / x = 0
proof
  arbitrary x:UInt
  assume zx: 0 < x
  expand operator/
  replace (apply eq_true to zx).
end

// Induction predicate used to prove quotient/remainder existence.
private fun UIntDivPred(n:UInt) {
  all m:UInt. if 0 < m then some r:UInt. (n / m) * m + r = n and r < m
}

// Every positive divisor has a quotient/remainder decomposition.
lemma uint_division: all n:UInt, m:UInt.
  if 0 < m
  then some r:UInt. (n/m)*m + r = n and r < m
proof
  have SI: all nn:UInt. if (all i:UInt. if i < nn then UIntDivPred(i))
                        then UIntDivPred(nn) by {
    arbitrary nn:UInt
    assume prem: all i:UInt. if i < nn then UIntDivPred(i)
    expand UIntDivPred
    arbitrary m:UInt
    assume m_pos: 0 < m
    switch nn < m {
      case true assume n_m {
        suffices some r:UInt. r = nn and r < m by {
          expand operator/
          simplify with n_m.
        }
        choose nn
        conclude nn = nn and nn < m by simplify with n_m.
      }
      case false assume not_n_m {
        have m_ne_z: not (m = 0) by apply uint_pos_not_zero to m_pos
        have m_le_n: m ≤ nn by apply uint_not_less_implies_less_equal to not_n_m
        have nm_n: nn ∸ m < nn by {
          have step1: (nn ∸ m) + m = nn by {
            replace uint_add_commute[nn ∸ m, m]
            apply uint_monus_add_identity[nn, m] to m_le_n
          }
          have step2: nn ∸ m < (nn ∸ m) + m
            by apply uint_less_add_pos[nn ∸ m, m] to expand lit | fromNat in m_pos
          replace step1 in step2
        }
        have IH_a: UIntDivPred(nn ∸ m) by apply prem to nm_n
        have IH_c: some r:UInt. ((nn ∸ m) / m) * m + r = (nn ∸ m) and r < m
          by apply (expand UIntDivPred in IH_a)[m] to m_pos
        obtain r0 where R: ((nn ∸ m) / m) * m + r0 = (nn ∸ m) and r0 < m from IH_c
        choose r0
        have conj0: (nn / m) * m + r0 = nn by {
          expand operator/
          replace (apply eq_false to not_n_m) | (apply eq_false to m_ne_z)
          show (1 + (nn ∸ m) / m) * m + r0 = nn
          replace uint_dist_mult_add_right[1, (nn ∸ m) / m, m]
          show m + ((nn ∸ m) / m) * m + r0 = nn
          replace conjunct 0 of R
          apply uint_monus_add_identity[nn, m] to m_le_n
        }
        conj0, conjunct 1 of R
      }
    }
  }
  arbitrary n:UInt
  have R: UIntDivPred(n) by apply uint_strong_induction[UIntDivPred, n] to SI
  expand UIntDivPred in R
end

// The quotient and remainder reconstruct the dividend.
theorem uint_div_mod: all n:UInt, m:UInt.
  if 0 < m
  then (n / m) * m + (n % m) = n
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  have ex: some r:UInt. (n/m)*m + r = n and r < m
    by apply uint_division[n, m] to m_pos
  obtain r where R: (n/m)*m + r = n and r < m from ex
  expand operator%
  define a = (n/m) * m
  have ar_n: a + r = n by R
  have a_le_n: a ≤ n by {
    have a_le_a_r: a ≤ a + r by uint_less_equal_add
    have eq_n_ar: n = a + r by symmetric (conjunct 0 of R)
    replace eq_n_ar
    a_le_a_r
  }
  have id: a + (n ∸ a) = n by apply uint_monus_add_identity[n, a] to a_le_n
  id
end

// The remainder is always smaller than a positive divisor.
theorem uint_mod_less_divisor: all n:UInt, m:UInt. if 0 < m then n % m < m
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  expand operator%
  obtain r where R: (n/m)*m + r = n and r < m
    from apply uint_division[n, m] to m_pos
  define a = (n/m)*m
  have ar_n: a + r = n by R
  have r_na: r = n ∸ a by {
    replace symmetric ar_n.
  }
  replace symmetric r_na
  conjunct 1 of R
end

// If the dividend is smaller than the divisor, the remainder is the dividend.
theorem uint_mod_small: all n:UInt, m:UInt. if n < m then n % m = n
proof
  arbitrary n:UInt, m:UInt
  assume n_m: n < m
  expand operator% | operator/
  replace (apply eq_true to n_m)
  uint_monus_zero[n]
end

// Divisibility: `a` divides `b` when `b` is a multiple of `a`.
fun divides(a : UInt, b : UInt) {
  some k:UInt. a * k = b
}

// Divisibility is reflexive.
theorem uint_divides_refl: all n:UInt. divides(n, n)
proof
  arbitrary n:UInt
  expand divides
  choose 1
  uint_mult_one[n]
end

// Every UInt divides zero.
theorem uint_divides_zero: all n:UInt. divides(n, 0)
proof
  arbitrary n:UInt
  expand divides
  choose 0
  uint_mult_zero[n]
end

// Divisibility is transitive.
theorem uint_divides_trans: all a:UInt, b:UInt, c:UInt.
  if divides(a, b) and divides(b, c) then divides(a, c)
proof
  arbitrary a:UInt, b:UInt, c:UInt
  assume prem
  obtain k where ak_b: a * k = b from expand divides in conjunct 0 of prem
  obtain l where bl_c: b * l = c from expand divides in conjunct 1 of prem
  expand divides
  choose k * l
  have eq1: (a * k) * l = c by replace symmetric ak_b in bl_c
  eq1
end

// Divisibility is closed under addition.
theorem uint_divides_add: all d:UInt, m:UInt, n:UInt.
  if divides(d, m) and divides(d, n) then divides(d, m + n)
proof
  arbitrary d:UInt, m:UInt, n:UInt
  assume prem
  obtain k where dk_m: d * k = m from expand divides in conjunct 0 of prem
  obtain l where dl_n: d * l = n from expand divides in conjunct 1 of prem
  expand divides
  choose k + l
  replace uint_dist_mult_add[d, k, l]
  replace dk_m | dl_n.
end

// Divisibility is closed under multiplying the divided value on the right.
theorem uint_divides_mult_right: all d:UInt, n:UInt, m:UInt.
  if divides(d, n) then divides(d, n * m)
proof
  arbitrary d:UInt, n:UInt, m:UInt
  assume dn
  obtain k where dk_n: d * k = n from expand divides in dn
  expand divides
  choose k * m
  replace dk_n.
end

// Divisibility is closed under multiplying the divided value on the left.
theorem uint_divides_mult_left: all d:UInt, n:UInt, m:UInt.
  if divides(d, n) then divides(d, m * n)
proof
  arbitrary d:UInt, n:UInt, m:UInt
  assume dn
  replace uint_mult_commute[m, n]
  apply uint_divides_mult_right[d, n, m] to dn
end

// A common divisor of two values also divides their truncated difference.
theorem uint_divides_monus: all d:UInt, m:UInt, n:UInt.
  if divides(d, m) and divides(d, n) then divides(d, m ∸ n)
proof
  arbitrary d:UInt, m:UInt, n:UInt
  assume prem
  obtain k where dk_m: d * k = m from expand divides in conjunct 0 of prem
  obtain l where dl_n: d * l = n from expand divides in conjunct 1 of prem
  expand divides
  choose k ∸ l
  replace uint_dist_mult_monus[d, k, l]
  replace dk_m | dl_n.
end

// If a divisor divides both `m` and `n`, it divides `m % n`.
theorem 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)
proof
  arbitrary d:UInt, m:UInt, n:UInt
  assume prem
  expand operator%
  have d_m: divides(d, m) by conjunct 0 of prem
  have d_n: divides(d, n) by conjunct 1 of prem
  have d_qn: divides(d, (m / n) * n)
    by apply uint_divides_mult_left[d, n, m / n] to d_n
  have both: divides(d, m) and divides(d, (m / n) * n) by d_m, d_qn
  apply uint_divides_monus[d, m, (m / n) * n] to both
end

// Euclidean algorithm for the greatest common divisor.
recfun gcd(a : UInt, b : UInt) -> UInt
  measure b of UInt
{
  if b = 0 then a
  else gcd(b, a % b)
}
terminates {
  arbitrary a:UInt, b:UInt
  assume bnz: not (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
}

theorem 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)
proof
  arbitrary d:UInt, m:UInt, n:UInt
  assume prem
  obtain k1 where dk1_n: d*k1 = n from expand divides in conjunct 0 of prem
  obtain k2 where dk2_mn: d*k2 = m % n from expand divides in conjunct 1 of prem
  have n_pos: 0 < n by prem
  have eq1: (m / n) * n + m % n = m by apply uint_div_mod[m, n] to n_pos
  expand divides
  have eq2: (m / n) * n + d*k2 = m by replace symmetric dk2_mn in eq1
  define X = m / n
  have eq3: (m / n)*d*k1 + d*k2 = m by expand X in replace symmetric dk1_n in eq2
  have eq4: d*(m/n)*k1 + d*k2 = m by replace uint_mult_commute[m/n, d] in eq3
  have eq5: d*((m/n)*k1 + k2) = m by replace symmetric uint_dist_mult_add[d, (m/n)*k1, k2] in eq4
  choose (m/n)*k1 + k2
  eq5
end

theorem uint_gcd_divides: all b:UInt, a:UInt. divides(gcd(a,b), a) and divides(gcd(a,b), b)
proof
  define P = fun b':UInt {all a:UInt. divides(gcd(a,b'), a) and divides(gcd(a,b'), b')}
  have X: all j:UInt. (if (all i:UInt. (if i < j then P(i))) then P(j)) by {
    arbitrary j:UInt
    assume IH: all i:UInt. (if i < j then P(i))
    expand P
    cases uint_zero_or_positive[j]
      case j_z {
        arbitrary a:UInt
        have A: divides(gcd(a, j), a) by {
          replace j_z
          expand divides | gcd
          choose 1
          conclude a * 1 = a by uint_mult_one
        }
        have B: divides(gcd(a, j), j) by {
          replace j_z
          expand divides | gcd
          choose 0
          conclude a * 0 = 0 by uint_mult_zero
        }
        A, B
      }
      case j_pos {
        arbitrary a:UInt
        have smaller: a % j < j
          by apply uint_mod_less_divisor[a,j] to j_pos
        have div_j_div_aj: divides(gcd(j, a % j), j) and divides(gcd(j, a % j), a % j)
          by (expand P in apply IH[a%j] to smaller)[j]
        have j_ne_z: not (j = 0) by apply uint_pos_not_zero to j_pos
        have A: divides(gcd(a, j), a) by {
          expand gcd
          replace apply eq_false to j_ne_z
          conclude divides(gcd(j, a % j), a)
            by apply uint_divides_mod[gcd(j, a % j), a, j] to div_j_div_aj, j_pos
        }
        have B: divides(gcd(a, j), j) by {
          expand gcd
          replace apply eq_false to j_ne_z
          conclude divides(gcd(j, a % j), j) by div_j_div_aj
        }
        A, B
      }
  }
  arbitrary b:UInt
  expand P in apply uint_strong_induction[P,b] to X
end

theorem uint_gcd_divides_left: all a:UInt, b:UInt. divides(gcd(a,b), a)
proof
  arbitrary a:UInt, b:UInt
  conjunct 0 of uint_gcd_divides[b, a]
end

theorem uint_gcd_divides_right: all a:UInt, b:UInt. divides(gcd(a,b), b)
proof
  arbitrary a:UInt, b:UInt
  conjunct 1 of uint_gcd_divides[b, a]
end

theorem uint_divides_less_equal: all a:UInt, b:UInt.
  if divides(a, b) and 0 < b then a ≤ b
proof
  arbitrary a:UInt, b:UInt
  assume prem
  obtain k where ak_b: a * k = b from expand divides in conjunct 0 of prem
  have k_ne_z: not (k = 0) by {
    assume k_z
    have a0_b: a * 0 = b by replace k_z in ak_b
    have z_b: 0 = b by a0_b
    have b_z: b = 0 by symmetric z_b
    have b_nz: not (b = 0) by apply uint_pos_not_zero to conjunct 1 of prem
    apply b_nz to b_z
  }
  have k_pos: 0 < k by apply uint_not_zero_pos to k_ne_z
  have one_le_k: 1 ≤ k by apply uint_pos_implies_one_le to k_pos
  have a_le_ak: a * 1 ≤ a * k by apply uint_mult_mono_le[a, 1, k] to one_le_k
  have a_le_ak2: a ≤ a * k by a_le_ak
  replace ak_b in a_le_ak2
end

theorem uint_divides_antisymmetric: all a:UInt, b:UInt.
  if divides(a, b) and divides(b, a) then a = b
proof
  arbitrary a:UInt, b:UInt
  assume prem
  cases uint_zero_or_positive[a]
  case a_z {
    obtain k where ak_b: a * k = b from expand divides in conjunct 0 of prem
    have z_b: 0 = b by replace a_z in ak_b
    have b_z: b = 0 by symmetric z_b
    replace a_z | b_z.
  }
  case a_pos {
    have b_ne_z: not (b = 0) by {
      assume b_z
      obtain k where bk_a: b * k = a from expand divides in conjunct 1 of prem
      have z_k_a: 0 * k = a by replace b_z in bk_a
      have z_a: 0 = a by z_k_a
      have a_z: a = 0 by symmetric z_a
      have a_ne_z: not (a = 0) by apply uint_pos_not_zero to a_pos
      apply a_ne_z to a_z
    }
    have b_pos: 0 < b by apply uint_not_zero_pos to b_ne_z
    have div_ab: divides(a, b) by conjunct 0 of prem
    have div_ba: divides(b, a) by conjunct 1 of prem
    have ab: divides(a, b) and 0 < b by div_ab, b_pos
    have ba: divides(b, a) and 0 < a by div_ba, a_pos
    have a_le_b: a ≤ b by apply uint_divides_less_equal[a, b] to ab
    have b_le_a: b ≤ a by apply uint_divides_less_equal[b, a] to ba
    apply uint_less_equal_antisymmetric to a_le_b, b_le_a
  }
end

theorem uint_gcd_greatest: all d:UInt, a:UInt, b:UInt.
  if divides(d, a) and divides(d, b) then divides(d, gcd(a,b))
proof
  define P = fun b':UInt {all a:UInt, d:UInt.
    if divides(d, a) and divides(d, b') then divides(d, gcd(a,b'))}
  have X: all j:UInt. (if (all i:UInt. (if i < j then P(i))) then P(j)) by {
    arbitrary j:UInt
    assume IH: all i:UInt. (if i < j then P(i))
    expand P
    cases uint_zero_or_positive[j]
      case j_z {
        arbitrary a:UInt, d:UInt
        assume prem
        replace j_z
        expand gcd
        conjunct 0 of prem
      }
      case j_pos {
        arbitrary a:UInt, d:UInt
        assume prem
        have smaller: a % j < j
          by apply uint_mod_less_divisor[a,j] to j_pos
        have d_aj: divides(d, a % j)
          by apply uint_divides_mod_of_divides[d, a, j] to prem
        have IH_aj: all a0:UInt, d0:UInt.
          if divides(d0, a0) and divides(d0, a % j) then divides(d0, gcd(a0, a % j))
          by expand P in apply IH[a%j] to smaller
        have j_ne_z: not (j = 0) by apply uint_pos_not_zero to j_pos
        expand gcd
        replace apply eq_false to j_ne_z
        have d_j: divides(d, j) by conjunct 1 of prem
        have both: divides(d, j) and divides(d, a % j) by d_j, d_aj
        apply IH_aj[j, d] to both
      }
  }
  arbitrary d:UInt, a:UInt, b:UInt
  assume prem
  have Pb: P(b) by apply uint_strong_induction[P,b] to X
  apply (expand P in Pb)[a, d] to prem
end

theorem uint_div_cancel: all y:UInt. if 0 < y then y / y = 1
proof
  arbitrary y:UInt
  assume y_pos
  have y_ne_zero: not (y = 0) by apply uint_pos_not_zero to y_pos
  expand operator/
  replace (apply eq_false to y_ne_zero)
  show 1 + 0 / y = 1
  replace (apply uint_zero_div to y_pos).
end

theorem uint_zero_mod: all x:UInt. 0 % x = 0
proof
  arbitrary x:UInt
  expand operator%
  expand lit | fromNat
  uint_bzero_monus
end

theorem uint_mod_self_zero: all y:UInt. y % y = 0
proof
  arbitrary y:UInt
  have y_z_p: y = 0 or 0 < y by uint_zero_or_positive[y]
  cases y_z_p
  case y_z {
    replace y_z
    uint_zero_mod
  }
  case y_pos {
    expand operator%
    have yyc: y/y = 1 by apply uint_div_cancel to y_pos
    replace yyc.
  }
end

theorem uint_mod_one: all n:UInt. n % 1 = 0
proof
  arbitrary n:UInt
  have one_pos: 0 < 1 by .
  have nm_lt_1: n % 1 < 1 by apply uint_mod_less_divisor[n, 1] to one_pos
  have nm_le_0: n % 1 ≤ 0
    by apply uint_less_add_one_implies_less_equal[n % 1, 0] to nm_lt_1
  apply uint_less_equal_zero to nm_le_0
end

theorem uint_div_one: all n:UInt. n / 1 = n
proof
  arbitrary n:UInt
  have one_pos: 0 < 1 by .
  have eq1: (n / 1) * 1 + (n % 1) = n by apply uint_div_mod[n, 1] to one_pos
  have eq2: (n / 1) + (n % 1) = n by eq1
  replace uint_mod_one in eq2
end

theorem uint_add_div_one: all n:UInt, m:UInt.
  if 0 < m
  then (n + m) / m = 1 + n / m
proof
  arbitrary n:UInt, m:UInt
  assume m_pos
  have m_nz: not (m = 0) by apply uint_pos_not_zero to m_pos
  have m_le_nm: m ≤ n + m by {
    have h: m ≤ m + n by uint_less_equal_add[m, n]
    replace uint_add_commute[m, n] in h
  }
  have not_nm_m: not (n + m < m) by {
    assume nm_m: n + m < m
    have nm_le_m: n + m ≤ m by apply uint_less_implies_less_equal to nm_m
    have eq_nm: n + m = m by apply uint_less_equal_antisymmetric to nm_le_m, m_le_nm
    have m_lt_m: m < m by replace eq_nm in nm_m
    apply uint_less_irreflexive to m_lt_m
  }
  equations
          (n + m) / m
        = 1 + ((n + m) ∸ m) / m  by {
            expand operator/
            replace (apply eq_false to not_nm_m)
                  | (apply eq_false to m_nz).
          }
    ... = 1 + n / m              by {
            replace uint_add_commute[n, m].
          }
end

theorem uint_mult_div_inverse: all n:UInt, m:UInt.
  (if 0 < m then (n * m) / m = n)
proof
  define P = fun n:UInt { all m:UInt. if 0 < m then (n * m) / m = n }
  have base_case: P(0) by {
    expand P
    arbitrary m:UInt
    assume m_pos
    show (0 * m) / m = 0
    apply uint_zero_div to m_pos
  }
  have ind: all n:UInt. if P(n) then P(1 + n) by {
    arbitrary n:UInt
    expand P
    assume IH: all m:UInt. if 0 < m then (n * m) / m = n
    arbitrary m:UInt
    assume m_pos
    show ((1 + n) * m) / m = 1 + n
    have eq1: (1 + n) * m = n * m + m by {
      replace uint_dist_mult_add_right[1, n, m]
      replace uint_add_commute[m, n * m].
    }
    replace eq1
    show (n * m + m) / m = 1 + n
    equations
      (n * m + m) / m = 1 + (n * m) / m  by apply uint_add_div_one[n * m, m] to m_pos
                  ... = 1 + n             by replace apply IH[m] to m_pos.
  }
  expand P in apply uint_induction[P] to base_case, ind
end

theorem uint_mult_div_left_inverse: all n:UInt, m:UInt.
  (if 0 < m then (m * n) / m = n)
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  replace uint_mult_commute[m, n]
  apply uint_mult_div_inverse[n, m] to m_pos
end

theorem uint_mult_mod_right_zero: all n:UInt, m:UInt.
  if 0 < m then (n * m) % m = 0
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  expand operator%
  replace (apply uint_mult_div_inverse[n, m] to m_pos)
  uint_monus_cancel[n * m]
end

theorem uint_mult_mod_left_zero: all n:UInt, m:UInt.
  if 0 < m then (m * n) % m = 0
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  replace uint_mult_commute[m, n]
  apply uint_mult_mod_right_zero[n, m] to m_pos
end

theorem uint_mult_add_div: all k:UInt, n:UInt, m:UInt.
  if 0 < m then (k * m + n) / m = k + n / m
proof
  define P = fun k:UInt { all n:UInt, m:UInt.
    if 0 < m then (k * m + n) / m = k + n / m }
  have base_case: P(0) by {
    expand P.
  }
  have ind: all k:UInt. if P(k) then P(1 + k) by {
    arbitrary k:UInt
    assume IH: P(k)
    expand P
    arbitrary n:UInt, m:UInt
    assume m_pos: 0 < m
    have step_arg: (1 + k) * m + n = (k * m + n) + m by {
      suffices toNat((1 + k) * m + n) = toNat((k * m + n) + m)
        by uint_toNat_injective
      replace toNat_add
      replace toNat_mult[1 + k, m] | toNat_mult[k, m]
      replace toNat_add[1, k] | toNat_add[n, m]
      have one_toNat: toNat(1) = ℕ1 by evaluate
      replace one_toNat
      replace dist_mult_add_right[ℕ1, toNat(k), toNat(m)]
      replace add_commute[toNat(m), toNat(k) * toNat(m)]
      replace add_commute[toNat(m), toNat(n)].
    }
    equations
      ((1 + k) * m + n) / m
          = ((k * m + n) + m) / m  by replace step_arg.
      ... = 1 + (k * m + n) / m    by apply uint_add_div_one[k * m + n, m] to m_pos
      ... = 1 + (k + n / m)        by {
              have IH_all: all n0:UInt, m0:UInt.
                if 0 < m0 then (k * m0 + n0) / m0 = k + n0 / m0
                by expand P in IH
              replace apply IH_all[n, m] to m_pos.
            }
      ... = (1 + k) + n / m        by .
  }
  expand P in apply uint_induction[P] to base_case, ind
end

theorem uint_add_mult_div: all n:UInt, k:UInt, m:UInt.
  if 0 < m then (n + k * m) / m = k + n / m
proof
  arbitrary n:UInt, k:UInt, m:UInt
  assume m_pos: 0 < m
  replace uint_add_commute[n, k * m]
  apply uint_mult_add_div[k, n, m] to m_pos
end

theorem uint_mult_add_mod: all k:UInt, n:UInt, m:UInt.
  if 0 < m then (k * m + n) % m = n % m
proof
  arbitrary k:UInt, n:UInt, m:UInt
  assume m_pos: 0 < m
  expand operator%
  replace (apply uint_mult_add_div[k, n, m] to m_pos)
  replace uint_dist_mult_add_right[k, n / m, m]
  uint_add_both_monus[k * m, n, (n / m) * m]
end

theorem uint_add_mult_mod: all n:UInt, k:UInt, m:UInt.
  if 0 < m then (n + k * m) % m = n % m
proof
  arbitrary n:UInt, k:UInt, m:UInt
  assume m_pos: 0 < m
  replace uint_add_commute[n, k * m]
  apply uint_mult_add_mod[k, n, m] to m_pos
end

theorem uint_mod_mod: all n:UInt, m:UInt.
  if 0 < m then (n % m) % m = n % m
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  have nm_lt_m: n % m < m by apply uint_mod_less_divisor[n, m] to m_pos
  apply uint_mod_small[n % m, m] to nm_lt_m
end

theorem uint_add_mod: all a:UInt, b:UInt, m:UInt.
  if 0 < m then (a + b) % m = ((a % m) + (b % m)) % m
proof
  arbitrary a:UInt, b:UInt, m:UInt
  assume m_pos: 0 < m
  have a_div: (a / m) * m + (a % m) = a
    by apply uint_div_mod[a, m] to m_pos
  have b_div: (b / m) * m + (b % m) = b
    by apply uint_div_mod[b, m] to m_pos
  have decomp:
    a + b = ((a / m) + (b / m)) * m + ((a % m) + (b % m)) by {
    suffices toNat(a + b) =
             toNat(((a / m) + (b / m)) * m + ((a % m) + (b % m)))
      by uint_toNat_injective
    have a_nat: toNat((a / m) * m + (a % m)) = toNat(a)
      by replace a_div.
    have b_nat: toNat((b / m) * m + (b % m)) = toNat(b)
      by replace b_div.
    have a_nat2: toNat(a / m) * toNat(m) + toNat(a % m) = toNat(a)
      by replace toNat_add | toNat_mult in a_nat
    have b_nat2: toNat(b / m) * toNat(m) + toNat(b % m) = toNat(b)
      by replace toNat_add | toNat_mult in b_nat
    replace toNat_add | toNat_mult
    replace symmetric a_nat2 | symmetric b_nat2
    replace toNat_add[a / m, b / m] | toNat_add[a % m, b % m]
    replace add_commute[toNat(a % m), toNat(b / m) * toNat(m)]
    replace symmetric dist_mult_add_right[toNat(a / m), toNat(b / m), toNat(m)].
  }
  replace decomp
  apply uint_mult_add_mod[(a / m) + (b / m), (a % m) + (b % m), m] to m_pos
end

theorem uint_mult_mod: all a:UInt, b:UInt, m:UInt.
  if 0 < m then (a * b) % m = ((a % m) * (b % m)) % m
proof
  arbitrary a:UInt, b:UInt, m:UInt
  assume m_pos: 0 < m
  have a_div: (a / m) * m + (a % m) = a
    by apply uint_div_mod[a, m] to m_pos
  have b_div: (b / m) * m + (b % m) = b
    by apply uint_div_mod[b, m] to m_pos
  have a_prod: a * b = ((a / m) * b) * m + (a % m) * b by {
    suffices toNat(a * b) = toNat(((a / m) * b) * m + (a % m) * b)
      by uint_toNat_injective
    have a_nat: toNat((a / m) * m + (a % m)) = toNat(a)
      by replace a_div.
    have a_nat2: toNat(a / m) * toNat(m) + toNat(a % m) = toNat(a)
      by replace toNat_add | toNat_mult in a_nat
    replace toNat_add | toNat_mult
    replace symmetric a_nat2
    replace toNat_mult[b, m]
    replace dist_mult_add_right[toNat(a / m) * toNat(m), toNat(a % m), toNat(b)]
    replace mult_commute[toNat(m), toNat(b)].
  }
  have a_zero: (((a / m) * b) * m) % m = 0
    by apply uint_mult_mod_right_zero[(a / m) * b, m] to m_pos
  have reduce_a: (a * b) % m = ((a % m) * b) % m by {
    equations
      (a * b) % m
          = ((((a / m) * b) * m + (a % m) * b) % m) by replace a_prod.
      ... = (((((a / m) * b) * m) % m) + (((a % m) * b) % m)) % m
            by apply uint_add_mod[((a / m) * b) * m, (a % m) * b, m] to m_pos
      ... = (0 + (((a % m) * b) % m)) % m by replace a_zero.
      ... = (((a % m) * b) % m) % m by .
      ... = ((a % m) * b) % m by apply uint_mod_mod[(a % m) * b, m] to m_pos
  }
  have b_prod: (a % m) * b = ((a % m) * (b / m)) * m + (a % m) * (b % m) by {
    suffices toNat((a % m) * b) = toNat(((a % m) * (b / m)) * m + (a % m) * (b % m))
      by uint_toNat_injective
    have b_nat: toNat((b / m) * m + (b % m)) = toNat(b)
      by replace b_div.
    have b_nat2: toNat(b / m) * toNat(m) + toNat(b % m) = toNat(b)
      by replace toNat_add | toNat_mult in b_nat
    replace toNat_add | toNat_mult
    replace symmetric b_nat2
    replace toNat_mult[b / m, m]
    replace dist_mult_add[toNat(a % m), toNat(b / m) * toNat(m), toNat(b % m)].
  }
  have b_zero: (((a % m) * (b / m)) * m) % m = 0
    by apply uint_mult_mod_right_zero[(a % m) * (b / m), m] to m_pos
  have reduce_b: ((a % m) * b) % m = ((a % m) * (b % m)) % m by {
    equations
      ((a % m) * b) % m
          = ((((a % m) * (b / m)) * m + (a % m) * (b % m)) % m)
            by replace b_prod.
      ... = (((((a % m) * (b / m)) * m) % m) + (((a % m) * (b % m)) % m)) % m
            by apply uint_add_mod[((a % m) * (b / m)) * m, (a % m) * (b % m), m] to m_pos
      ... = (0 + (((a % m) * (b % m)) % m)) % m by replace b_zero.
      ... = (((a % m) * (b % m)) % m) % m by .
      ... = ((a % m) * (b % m)) % m by apply uint_mod_mod[(a % m) * (b % m), m] to m_pos
  }
  equations
    (a * b) % m = ((a % m) * b) % m by reduce_a
    ... = ((a % m) * (b % m)) % m by reduce_b
end

theorem uint_div_less_equal: all n:UInt, m:UInt.
  if 0 < m then n / m ≤ n
proof
  arbitrary n:UInt, m:UInt
  assume m_pos: 0 < m
  have one_le_m: 1 ≤ m by apply uint_pos_implies_one_le to m_pos
  have q_le_qm: (n / m) * 1 ≤ (n / m) * m
    by apply uint_mult_mono_le[n / m, 1, m] to one_le_m
  have qm_le_n: (n / m) * m ≤ n by {
    have qmr: (n / m) * m ≤ (n / m) * m + (n % m) by uint_less_equal_add
    replace apply uint_div_mod[n, m] to m_pos in qmr
  }
  apply uint_less_equal_trans to q_le_qm, qm_le_n
end

theorem uint_div_less: all n:UInt, m:UInt.
  if 0 < n and 1 < m then n / m < n
proof
  arbitrary n:UInt, m:UInt
  assume prem
  have n_pos: 0 < n by prem
  have one_lt_m: 1 < m by prem
  have zero_lt_one: 0 < 1 by .
  have m_pos: 0 < m by apply uint_less_trans to zero_lt_one, one_lt_m
  have q_le_n: n / m ≤ n by apply uint_div_less_equal[n, m] to m_pos
  cases expand operator≤ in q_le_n
  case q_lt_n: n / m < n {
    q_lt_n
  }
  case q_eq_n: n / m = n {
    have n_lt_nm: n < n * m by {
      have q_pos: 0 < n / m by replace symmetric q_eq_n in n_pos
      have q_lt_qm: (n / m) * 1 < (n / m) * m
        by apply uint_pos_mult_both_sides_of_less[n / m, 1, m] to q_pos, one_lt_m
      replace q_eq_n in q_lt_qm
    }
    have nm_le_n: n * m ≤ n by {
      have qm_le_n: (n / m) * m ≤ n by {
        have qmr: (n / m) * m ≤ (n / m) * m + (n % m) by uint_less_equal_add
        replace apply uint_div_mod[n, m] to m_pos in qmr
      }
      replace q_eq_n in qm_le_n
    }
    have nat_n_lt_nm: toNat(n) < toNat(n * m) by apply toNat_less to n_lt_nm
    have nat_nm_le_n: toNat(n * m) ≤ toNat(n) by apply toNat_less_equal to nm_le_n
    have nat_n_lt_n: toNat(n) < toNat(n)
      by apply less_le_trans[toNat(n), toNat(n * m), toNat(n)] to nat_n_lt_nm, nat_nm_le_n
    conclude false by apply less_irreflexive to nat_n_lt_n
  }
end

theorem uint_div_zero: all n:UInt. n / 0 = 0
proof
  arbitrary n:UInt
  expand operator/
  replace (apply eq_false to uint_not_less_zero[n]).
end

theorem fromNat_div: all x:Nat, y:Nat. fromNat(x) / fromNat(y) = fromNat(x / y)
proof
  have lem: all y:Nat. all x:Nat. fromNat(x) / fromNat(y) = fromNat(x / y) by {
    arbitrary y:Nat
    cases nat_zero_or_positive[y]
    case y_z {
      arbitrary x:Nat
      replace y_z
      have xz: x / ℕ0 = ℕ0 by expand operator/ | lit.
      replace xz
      uint_div_zero[fromNat(x)]
    }
    case y_pos {
      have y_pos_nat: zero < y by expand lit in y_pos
      have y_ne_zero: not (y = zero) by {
        assume y_z
        replace y_z in y_pos_nat
      }
      have fy_pos: 0 < fromNat(y) by replace from_zero in apply less_fromNat to y_pos
      have fy_ne_zero: not (fromNat(y) = 0) by apply uint_pos_not_zero to fy_pos
      define P = fun x:Nat { fromNat(x) / fromNat(y) = fromNat(x / y) }
      have SI: all i:Nat. if (all j:Nat. if j < i then P(j)) then P(i) by {
        arbitrary i:Nat
        assume IH: all j:Nat. if j < i then P(j)
        expand P
        switch i < y {
          case true assume i_y_t {
            have i_less_y: i < y by simplify with i_y_t.
            have fi_less_fy: fromNat(i) < fromNat(y) by apply less_fromNat to i_less_y
            have lhs_zero: fromNat(i) / fromNat(y) = 0 by {
              expand operator/
              replace (apply eq_true to fi_less_fy).
            }
            have rhs_zero: i / y = zero by {
              expand operator/
              replace (apply eq_true to i_less_y).
            }
            replace lhs_zero | rhs_zero
            expand lit.
          }
          case false assume i_y_f {
            have not_i_y: not (i < y) by i_y_f
            have y_le_i: y ≤ i by apply not_less_implies_less_equal to not_i_y
            have not_fi_fy: not (fromNat(i) < fromNat(y)) by {
              assume fi_fy
              have A: toNat(fromNat(i)) < toNat(fromNat(y)) by apply toNat_less to fi_fy
              have i_less_y: i < y by replace uint_toNat_fromNat in A
              apply not_i_y to i_less_y
            }
            have monus_eq: fromNat(i) ∸ fromNat(y) = fromNat(i ∸ y) by {
              suffices toNat(fromNat(i) ∸ fromNat(y)) = toNat(fromNat(i ∸ y))
                by uint_toNat_injective
              replace toNat_monus | uint_toNat_fromNat.
            }
            have im_less_i: i ∸ y < i by {
              suffices y + (i ∸ y) < y + i by add_both_sides_of_less[y, i ∸ y, i]
              suffices i < y + i by replace apply monus_add_identity[i, y] to y_le_i.
              replace add_commute[y, i]
              apply nat_less_add_pos[i, y] to y_pos
            }
            have ih_app: P(i ∸ y) by apply IH to im_less_i
            have ih_eq: fromNat(i ∸ y) / fromNat(y) = fromNat((i ∸ y) / y)
              by expand P in ih_app
            have rhs_step: i / y = suc(zero) + (i ∸ y) / y by {
              equations
                i / y
                    = suc(zero) + (i ∸ y) / y by {
                        expand operator/
                        replace (apply eq_false to not_i_y)
                              | (apply eq_false to y_ne_zero).
                      }
            }
            equations
              fromNat(i) / fromNat(y)
                  = 1 + (fromNat(i) ∸ fromNat(y)) / fromNat(y)   by {
                      expand operator/
                      replace (apply eq_false to not_fi_fy)
                            | (apply eq_false to fy_ne_zero).
                    }
              ... = 1 + fromNat(i ∸ y) / fromNat(y)              by replace monus_eq.
              ... = 1 + fromNat((i ∸ y) / y)                     by replace ih_eq.
              ... = fromNat(lit(suc(zero)) + (i ∸ y) / y)        by symmetric fromNat_add[lit(suc(zero)), (i ∸ y) / y]
              ... = fromNat(suc(zero) + (i ∸ y) / y)             by expand lit.
              ... = # fromNat(i / y) #                           by replace rhs_step.
          }
        }
      }
      arbitrary x:Nat
      have hx: P(x) by apply strong_induction[P, x] to SI
      expand P in hx
    }
  }
  arbitrary x:Nat, y:Nat
  lem[y, x]
end

theorem fromNat_mod: all x:Nat, y:Nat. fromNat(x) % fromNat(y) = fromNat(x % y)
proof
  arbitrary x:Nat, y:Nat
  suffices toNat(fromNat(x) % fromNat(y)) = toNat(fromNat(x % y))
    by uint_toNat_injective
  expand operator%
  replace toNat_monus | toNat_mult | fromNat_div | uint_toNat_fromNat.
end

theorem toNat_mod: all x:UInt, y:UInt. toNat(x % y) = toNat(x) % toNat(y)
proof
  arbitrary x:UInt, y:UInt
  replace symmetric uint_fromNat_toNat[x]
  replace symmetric uint_fromNat_toNat[y]
  replace fromNat_mod[toNat(x), toNat(y)]
  replace uint_toNat_fromNat[toNat(x)]
  replace uint_toNat_fromNat[toNat(y)]
  uint_toNat_fromNat[toNat(x) % toNat(y)]
end

theorem uint_lit_div: all x:Nat, y:Nat. (fromNat(lit(x)) / fromNat(lit(y))) = fromNat(lit(x) / lit(y))
proof
  arbitrary x:Nat, y:Nat
  fromNat_div[lit(x), lit(y)]
end

auto uint_lit_div