module BigO

import UInt
import List

/*
  Elementary asymptotic notation for functions `UInt -> UInt`.

  The relation `f ≲ g` means that, after some threshold `n0`, `f` is
  bounded above by a constant multiple of `g`. The relation `f ≈ g`
  is the induced two-sided equivalence.
*/

// Pointwise addition of cost functions.
fun operator + (f : fn UInt -> UInt, g : fn UInt -> UInt) {
  fun x:UInt {
    f(x) + g(x)
  }
}

// Pointwise multiplication of cost functions.
fun operator * (f : fn UInt -> UInt, g : fn UInt -> UInt) {
  fun x:UInt {
    f(x) * g(x)
  }
}

// Scale a cost function by a constant.
fun operator * (k : UInt, g : fn UInt -> UInt) {
  fun x:UInt {
    k * g(x)
  }
}

// Big-O preorder.
fun operator ≲ (f : fn UInt -> UInt, g : fn UInt -> UInt) {
  some n0 :UInt, c:UInt. all n:UInt. if n0 ≤ n then f(n) ≤ c * g(n)
}

// Asymptotic equivalence.
fun operator ≈ (f : fn UInt -> UInt, g : fn UInt -> UInt) {
  (f ≲ g) and (g ≲ f)
}

// Pointwise log of a cost function (lifts `UInt` `log` from values to functions).
fun log(f : fn UInt -> UInt) {
  fun x:UInt { log(f(x)) }
}


// Constant Time
fun O_1(n:UInt) { 1 }

// Logarithmic Time
fun O_log(n:UInt) { log(n) }

// Linear Time
fun O_n(n:UInt) { n }

// Quadratic Time
fun O_n2(n:UInt) { n * n }

// Big-O preorder is reflexive: every function is ≲ itself (`n0 = 0`, `c = 1`).
theorem bigo_refl: all f : fn UInt -> UInt. f ≲ f
proof
  arbitrary f : fn UInt -> UInt
  expand operator≲
  choose 0, 1
  arbitrary n:UInt
  assume prem
  show f(n) ≤ 1 * f(n)
  uint_less_equal_refl
end

// Big-O preorder is transitive: thresholds add and constants multiply.
theorem bigo_trans: all f : fn UInt -> UInt, g : fn UInt -> UInt, h : fn UInt -> UInt.
  if f ≲ g and g ≲ h then f ≲ h
proof
  arbitrary f : fn UInt -> UInt, g : fn UInt -> UInt, h : fn UInt -> UInt
  assume prem
  have fg: f ≲ g by prem
  obtain n1, c1 where fg_all: all n:UInt. if n1 ≤ n then f(n) ≤ c1 * g(n)
    from expand operator≲ in fg
  have gh: g ≲ h by prem
  obtain n2, c2 where gh_all: all n:UInt. if n2 ≤ n then g(n) ≤ c2 * h(n)
    from expand operator≲ in gh
  expand operator≲
  choose n1+n2, c1*c2
  arbitrary n:UInt
  assume n12_n
  show f(n) ≤ (c1 * c2) * h(n)

  have n1_n: n1 ≤ n by {
    have n1_n12: n1 ≤ n1 + n2 by uint_less_equal_add
    apply uint_less_equal_trans to n1_n12, n12_n
  }
  have fg_n: f(n) ≤ c1 * g(n) by apply fg_all to n1_n
  
  have n2_n: n2 ≤ n by {
    have n2_n21: n2 ≤ n1 + n2 by { replace uint_add_commute uint_less_equal_add }
    apply uint_less_equal_trans to n2_n21, n12_n
  }
  have gh_n: g(n) ≤ c2 * h(n) by apply gh_all to n2_n

  have c1g_c12_h: c1 * g(n) ≤ c1 * c2 * h(n)
    by apply uint_mult_mono_le[c1, g(n), c2*h(n)] to gh_n
  
  conclude f(n) ≤ c1 * c2 * h(n)
    by apply uint_less_equal_trans to fg_n, c1g_c12_h
end

// Adding a function to itself stays asymptotically bounded by it (`c = 2`).
theorem bigo_add: all f: fn UInt->UInt. f + f ≲ f
proof
  arbitrary f: fn UInt->UInt
  expand operator≲
  choose 0, 2
  arbitrary n:UInt
  assume prem
  expand operator+
  show f(n) + f(n) ≤ 2 * f(n)
  replace uint_two_mult.
end

// Any constant multiple of `f` is ≲ `f` — constant factors are absorbed by `c`.
theorem bigo_const_mult: all f: fn UInt -> UInt, k:UInt.
  k * f ≲ f
proof
  arbitrary f: fn UInt -> UInt
  define P = fun c:UInt { c * f ≲ f }
  have base: P(0) by {
    expand P | operator≲ | operator*.
  }
  have ind: all m:UInt. if P(m) then P(1 + m) by {
    arbitrary m:UInt
    expand P
    assume mf_f: m * f ≲ f 
    obtain n0, c where mf_f_all: all n:UInt. if n0 ≤ n then m * f(n) ≤ c * f(n)
      from expand operator≲ | operator* in mf_f
    expand operator≲
    choose n0, 2*(1 + c)
    arbitrary n:UInt
    assume n0_n
    expand operator*
    replace uint_dist_mult_add_right | uint_dist_mult_add
    show f(n) + m * f(n) ≤ 2 * f(n) + 2 * c * f(n)
    
    have fn_cfn: f(n) ≤ 2 * f(n) by replace uint_two_mult uint_less_equal_add
    have mfn_2cfn: m * f(n) ≤ 2 * c * f(n) by {
      have IH: m * f(n) ≤ c * f(n) by apply mf_f_all[n] to n0_n
      have cfn_2cfn: c * f(n) ≤ 2 * c * f(n) by {
        apply uint_mult_mono_le2[1,c*f(n),2,c*f(n)] to .
      }
      apply uint_less_equal_trans to IH, cfn_2cfn
    }
    conclude f(n) + m * f(n) ≤ 2 * f(n) + 2 * c * f(n)
      by apply uint_add_mono_less_equal to fn_cfn, mfn_2cfn
  }
  expand P in apply uint_induction[P] to base, ind
end

// Pointwise multiplication is monotone in both arguments under ≲.
theorem bigo_mult_mono:
  all f1: fn UInt->UInt, f2: fn UInt->UInt, g1: fn UInt->UInt, g2: fn UInt->UInt.
  if f1 ≲ g1 and f2 ≲ g2
  then f1 * f2 ≲ g1 * g2
proof
  arbitrary f1: fn UInt->UInt, f2: fn UInt->UInt, g1: fn UInt->UInt, g2: fn UInt->UInt
  assume prem
  expand operator≲ | operator*
  have f1_g1: f1 ≲ g1 by prem
  obtain n1, c1 where f1_c1g1_all: all n:UInt. if n1 ≤ n then f1(n) ≤ c1 * g1(n)
    from expand operator≲ in f1_g1
  have f2_g2: f2 ≲ g2 by prem
  obtain n2, c2 where f2_c2g2_all: all n:UInt. if n2 ≤ n then f2(n) ≤ c2 * g2(n)
    from expand operator≲ in f2_g2
  choose n1 + n2, c1 * c2
  arbitrary n:UInt
  assume n12_n: n1 + n2 ≤ n
  show f1(n) * f2(n) ≤ c1 * c2 * g1(n) * g2(n)

  have n1_n: n1 ≤ n by {
    have n1_n12: n1 ≤ n1 + n2 by uint_less_equal_add
    apply uint_less_equal_trans to n1_n12, n12_n
  }
  have f1_c1g1: f1(n) ≤ c1 * g1(n)
    by apply f1_c1g1_all to n1_n
  
  have n2_n: n2 ≤ n by {
    have n2_n12: n2 ≤ n1 + n2 by { replace uint_add_commute uint_less_equal_add }
    apply uint_less_equal_trans to n2_n12, n12_n
  }
  have f2_c2g2: f2(n) ≤ c2 * g2(n)
    by apply f2_c2g2_all to n2_n
  
  have f12_c1g1_c2g2: f1(n) * f2(n) ≤ c1 * g1(n) * c2 * g2(n)
    by apply uint_mult_mono_le2[f1(n), f2(n)] to f1_c1g1, f2_c2g2

  conclude f1(n) * f2(n) ≤ c1 * c2 * g1(n) * g2(n)
    by replace uint_mult_commute[g1(n),c2] in f12_c1g1_c2g2
end

// Pointwise ordering of cost functions implies asymptotic ordering.
theorem bigo_pointwise_le: all f:fn UInt->UInt, g:fn UInt->UInt.
  if (all n:UInt. f(n) ≤ g(n)) then f ≲ g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H
  expand operator≲
  choose 0, 1
  arbitrary n:UInt
  assume _
  show f(n) ≤ 1 * g(n)
  H
end

// Each summand is bounded above by the sum.
theorem bigo_self_le_add: all f:fn UInt->UInt, g:fn UInt->UInt. f ≲ f + g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≲ | operator+
  choose 0, 1
  arbitrary n:UInt
  assume _
  show f(n) ≤ 1 * (f(n) + g(n))
  uint_less_equal_add
end

// Sibling of `bigo_self_le_add`: the right summand is bounded by the sum.
theorem bigo_le_add_self: all f:fn UInt->UInt, g:fn UInt->UInt. g ≲ f + g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≲ | operator+
  choose 0, 1
  arbitrary n:UInt
  assume _
  show g(n) ≤ 1 * (f(n) + g(n))
  uint_less_equal_add_left
end

// Asymptotic equivalence is reflexive, symmetric, and transitive.
theorem bigo_equiv_refl: all f:fn UInt->UInt. f ≈ f
proof
  arbitrary f:fn UInt->UInt
  expand operator≈
  have rf: f ≲ f by bigo_refl
  rf, rf
end

// Symmetry of ≈: swap the two ≲ directions.
theorem bigo_equiv_sym: all f:fn UInt->UInt, g:fn UInt->UInt.
  if f ≈ g then g ≈ f
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H
  have fg: f ≲ g by expand operator≈ in H
  have gf: g ≲ f by expand operator≈ in H
  expand operator≈
  gf, fg
end

// Transitivity of ≈, via `bigo_trans` on each direction.
theorem bigo_equiv_trans:
  all f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt.
  if f ≈ g and g ≈ h then f ≈ h
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt
  assume prem
  have fg: f ≈ g by prem
  have gh: g ≈ h by prem
  have f_g: f ≲ g by expand operator≈ in fg
  have g_f: g ≲ f by expand operator≈ in fg
  have g_h: g ≲ h by expand operator≈ in gh
  have h_g: h ≲ g by expand operator≈ in gh
  have fh: f ≲ h by apply bigo_trans to f_g, g_h
  have hf: h ≲ f by apply bigo_trans to h_g, g_f
  expand operator≈
  fh, hf
end

// Additivity of ≲: pointwise sum is monotone in both arguments.
theorem bigo_add_mono:
  all f1:fn UInt->UInt, f2:fn UInt->UInt, g1:fn UInt->UInt, g2:fn UInt->UInt.
  if f1 ≲ g1 and f2 ≲ g2 then f1 + f2 ≲ g1 + g2
proof
  arbitrary f1:fn UInt->UInt, f2:fn UInt->UInt, g1:fn UInt->UInt, g2:fn UInt->UInt
  assume prem
  have f1g1: f1 ≲ g1 by prem
  obtain n1, c1 where f1_g1_all: all n:UInt. if n1 ≤ n then f1(n) ≤ c1 * g1(n)
    from expand operator≲ in f1g1
  have f2g2: f2 ≲ g2 by prem
  obtain n2, c2 where f2_g2_all: all n:UInt. if n2 ≤ n then f2(n) ≤ c2 * g2(n)
    from expand operator≲ in f2g2
  expand operator≲ | operator+
  choose n1 + n2, c1 + c2
  arbitrary n:UInt
  assume n12_n: n1 + n2 ≤ n
  show f1(n) + f2(n) ≤ (c1 + c2) * (g1(n) + g2(n))

  have n1_n12: n1 ≤ n1 + n2 by uint_less_equal_add
  have n1_n: n1 ≤ n by apply uint_less_equal_trans to n1_n12, n12_n
  have n2_n12: n2 ≤ n1 + n2 by uint_less_equal_add_left
  have n2_n: n2 ≤ n by apply uint_less_equal_trans to n2_n12, n12_n

  have f1_le: f1(n) ≤ c1 * g1(n) by apply f1_g1_all to n1_n
  have f2_le: f2(n) ≤ c2 * g2(n) by apply f2_g2_all to n2_n

  have c1_le: c1 ≤ c1 + c2 by uint_less_equal_add
  have c2_le: c2 ≤ c1 + c2 by uint_less_equal_add_left
  have g1_le: g1(n) ≤ g1(n) by .
  have g2_le: g2(n) ≤ g2(n) by .

  have step_c1: c1 * g1(n) ≤ (c1 + c2) * g1(n)
    by apply uint_mult_mono_le2 to c1_le, g1_le
  have step_c2: c2 * g2(n) ≤ (c1 + c2) * g2(n)
    by apply uint_mult_mono_le2 to c2_le, g2_le

  have f1_bigger: f1(n) ≤ (c1 + c2) * g1(n)
    by apply uint_less_equal_trans to f1_le, step_c1
  have f2_bigger: f2(n) ≤ (c1 + c2) * g2(n)
    by apply uint_less_equal_trans to f2_le, step_c2

  have step_add: f1(n) + f2(n) ≤ (c1 + c2) * g1(n) + (c1 + c2) * g2(n)
    by apply uint_add_mono_less_equal to f1_bigger, f2_bigger

  conclude f1(n) + f2(n) ≤ (c1 + c2) * (g1(n) + g2(n))
    by replace uint_dist_mult_add
       step_add
end

// Pointwise addition is commutative up to ≈.
theorem bigo_add_commute: all f:fn UInt->UInt, g:fn UInt->UInt.
  f + g ≈ g + f
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≈
  have A: f + g ≲ g + f by {
    expand operator≲ | operator+
    choose 0, 1
    arbitrary n:UInt
    assume _
    show f(n) + g(n) ≤ 1 * (g(n) + f(n))
    replace uint_add_commute[g(n), f(n)].
  }
  have B: g + f ≲ f + g by {
    expand operator≲ | operator+
    choose 0, 1
    arbitrary n:UInt
    assume _
    show g(n) + f(n) ≤ 1 * (f(n) + g(n))
    replace uint_add_commute[f(n), g(n)].
  }
  A, B
end

// Pointwise multiplication is commutative up to ≈.
theorem bigo_mult_commute: all f:fn UInt->UInt, g:fn UInt->UInt.
  f * g ≈ g * f
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≈
  have A: f * g ≲ g * f by {
    expand operator≲ | operator*
    choose 0, 1
    arbitrary n:UInt
    assume _
    show f(n) * g(n) ≤ 1 * (g(n) * f(n))
    replace uint_mult_commute[g(n), f(n)].
  }
  have B: g * f ≲ f * g by {
    expand operator≲ | operator*
    choose 0, 1
    arbitrary n:UInt
    assume _
    show g(n) * f(n) ≤ 1 * (f(n) * g(n))
    replace uint_mult_commute[f(n), g(n)].
  }
  A, B
end

// Sum absorption: a dominated summand can be dropped.
theorem bigo_add_absorb: all f:fn UInt->UInt, g:fn UInt->UInt.
  if g ≲ f then f + g ≲ f
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume g_f: g ≲ f
  have f_f: f ≲ f by bigo_refl
  have step: f + g ≲ f + f
    by apply bigo_add_mono to f_f, g_f
  have ff: f + f ≲ f by bigo_add
  apply bigo_trans to step, ff
end

// Multiplying by a constant k ≥ 1 only increases asymptotic cost.
theorem bigo_le_const_mult: all f:fn UInt->UInt, k:UInt.
  if 1 ≤ k then f ≲ k * f
proof
  arbitrary f:fn UInt->UInt, k:UInt
  assume k_pos: 1 ≤ k
  expand operator≲ | operator*
  choose 0, 1
  arbitrary n:UInt
  assume _
  show f(n) ≤ 1 * (k * f(n))
  have fn_fn: f(n) ≤ f(n) by .
  have step: 1 * f(n) ≤ k * f(n)
    by apply uint_mult_mono_le2 to k_pos, fn_fn
  step
end

// Any constant function is O(1).
theorem bigo_const_func_le_O_1: all c:UInt.
  (fun n:UInt { c }) ≲ O_1
proof
  arbitrary c:UInt
  expand operator≲ | O_1
  choose 0, c
  arbitrary n:UInt
  assume _
  show c ≤ c * 1
  .
end

// Hierarchy: constant ≲ log. For n ≥ 2, log(n) ≥ 1.
theorem constant_le_log: O_1 ≲ O_log
proof
  expand operator≲ | O_1 | O_log
  choose 2, 1
  arbitrary n:UInt
  assume two_n
  apply uint_log_greater_one to two_n
end

// Hierarchy: log ≲ linear, since `log(n) ≤ n` for every `n`.
theorem log_le_linear: O_log ≲ O_n
proof
  expand operator≲ | O_log | O_n
  choose 0, 1
  arbitrary n:UInt
  assume _
  uint_logn_le_n
end

// Hierarchy: linear ≲ quadratic. For n ≥ 1, n ≤ n * n.
theorem linear_le_quadratic: O_n ≲ O_n2
proof
  expand operator≲ | O_n | O_n2
  choose 1, 1
  arbitrary n:UInt
  assume pos
  have n_n: n ≤ n by .
  conclude 1 * n ≤ n * n by apply uint_mult_mono_le2 to pos, n_n
end

// `2n` cost class: spelled out as a named function so the constant factor
// can be shown to drop under ≈ in `O_n_eq_O_2n`.
fun O_2n(n:UInt) { 2*n }

// Constant factors drop in ≈: linear and `2n` are asymptotically the same.
theorem O_n_eq_O_2n: O_n ≈ O_2n
proof
  expand operator≈
  have A: O_n ≲ O_2n by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    expand O_n | O_2n
    replace uint_two_mult
    uint_less_equal_add
  }
  have B: O_2n ≲ O_n by {
    expand operator≲
    choose 0, 2
    arbitrary n:UInt
    assume prem
    expand O_n | O_2n.
  }
  A, B
end

// Pointwise positivity: every value of `f` is strictly positive.
fun positive(f : fn UInt -> UInt) {
  all n:UInt. 0 < f(n)
}

// One direction of the log-product law (under `1 < f, g`):
// `log(f*g) ≲ log(f) + log(g)`, via the pointwise `log(a*b) ≤ 1 + log(a) + log(b)`.
theorem log_product_less_equal_sum:
  all f:fn UInt -> UInt, g:fn UInt -> UInt.
  if (all n:UInt. 1 < f(n)) and (all n:UInt. 1 < g(n))
  then log(f * g) ≲ log(f) + log(g)
proof
  arbitrary f:fn UInt -> UInt, g:fn UInt -> UInt
  assume fg_gt_1
  expand operator≲ | operator+ | operator* | log
  choose 0, 2
  arbitrary n:UInt
  assume _
  have A: log(f(n) * g(n)) ≤ 1 + log(f(n)) + log(g(n)) by uint_log_mult_le_log_add
  have B: 1 + log(f(n)) + log(g(n)) ≤ 2 * (log(f(n)) + log(g(n))) by {
    have log_fg_pos: 0 < log(f(n)) + log(g(n)) by {
      have log_f_pos: 0 < log(f(n)) by apply uint_log_pos[f(n)] to fg_gt_1
      have log_g_pos: 0 < log(g(n)) by apply uint_log_pos[g(n)] to fg_gt_1
      apply uint_add_mono_less[0, 0, log(f(n)), log(g(n))] to log_f_pos, log_g_pos
    }
    replace uint_two_mult
    apply uint_add_one_le_double to log_fg_pos
  }
  apply uint_less_equal_trans to A, B
end

// Converse direction (under positivity): `log(f) + log(g) ≲ log(f*g)`.
theorem log_sum_less_equal_product:
  all f:fn UInt -> UInt, g:fn UInt -> UInt.
  if (all n:UInt. 0 < f(n)) and (all n:UInt. 0 < g(n))
  then log(f) + log(g) ≲ log(f * g)
proof
  arbitrary f:fn UInt -> UInt, g:fn UInt -> UInt
  assume fg_pos
  expand operator≲ | operator+ | operator* | log
  choose 0, 1
  arbitrary n:UInt
  assume _
  have f_pos: 0 < f(n) by fg_pos
  have g_pos: 0 < g(n) by fg_pos
  apply uint_log_add_le_log_mult to f_pos, g_pos
end

// Two-sided log-product law (under `1 < f, g`): `log(f*g) ≈ log(f) + log(g)`.
theorem log_product_equiv_sum:
  all f:fn UInt -> UInt, g:fn UInt -> UInt.
  if (all n:UInt. 1 < f(n)) and (all n:UInt. 1 < g(n))
  then log(f * g) ≈ log(f) + log(g)
proof
  arbitrary f:fn UInt -> UInt, g:fn UInt -> UInt
  assume fg_gt_1
  expand operator≈
  have A: log(f * g) ≲ log(f) + log(g) by apply log_product_less_equal_sum[f,g] to fg_gt_1
  have f_pos: all n:UInt. 0 < f(n) by {
    arbitrary n:UInt
    have one_lt_f: 1 < f(n) by fg_gt_1
    have zero_lt_one: (0:UInt) < 1 by .
    apply uint_less_trans to zero_lt_one, one_lt_f
  }
  have g_pos: all n:UInt. 0 < g(n) by {
    arbitrary n:UInt
    have one_lt_g: 1 < g(n) by fg_gt_1
    have zero_lt_one: (0:UInt) < 1 by .
    apply uint_less_trans to zero_lt_one, one_lt_g
  }
  have B: log(f) + log(g) ≲ log(f * g)
    by apply log_sum_less_equal_product[f,g] to f_pos, g_pos
  A, B
end

// Pointwise equality lifts to asymptotic equivalence.
theorem bigo_pointwise_eq: all f:fn UInt->UInt, g:fn UInt->UInt.
  if (all n:UInt. f(n) = g(n)) then f ≈ g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H
  expand operator≈
  have fg: f ≲ g by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show f(n) ≤ 1 * g(n)
    have eq: f(n) = g(n) by H
    replace eq.
  }
  have gf: g ≲ f by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show g(n) ≤ 1 * f(n)
    have eq: f(n) = g(n) by H
    replace symmetric eq.
  }
  fg, gf
end

// Pointwise addition is associative up to ≈.
theorem bigo_add_assoc: all f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt.
  (f + g) + h ≈ f + (g + h)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt
  have pointwise: all m:UInt. ((f + g) + h)(m) = (f + (g + h))(m) by {
    arbitrary m:UInt
    expand operator+.
  }
  apply bigo_pointwise_eq[(f + g) + h, f + (g + h)] to pointwise
end

// Pointwise multiplication is associative up to ≈.
theorem bigo_mult_assoc: all f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt.
  (f * g) * h ≈ f * (g * h)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt
  have pointwise: all m:UInt. ((f * g) * h)(m) = (f * (g * h))(m) by {
    arbitrary m:UInt
    expand operator*.
  }
  apply bigo_pointwise_eq[(f * g) * h, f * (g * h)] to pointwise
end

// The zero cost function is a right identity for + up to ≈.
theorem bigo_add_zero: all f:fn UInt->UInt.
  f + (fun n:UInt { 0 }) ≈ f
proof
  arbitrary f:fn UInt->UInt
  have pointwise: all m:UInt. (f + (fun n:UInt { 0 }))(m) = f(m) by {
    arbitrary m:UInt
    expand operator+.
  }
  apply bigo_pointwise_eq[f + (fun n:UInt { 0 }), f] to pointwise
end

// The constant-1 function is a right identity for * up to ≈.
theorem bigo_mult_one_func: all f:fn UInt->UInt.
  f * (fun n:UInt { 1 }) ≈ f
proof
  arbitrary f:fn UInt->UInt
  have pointwise: all m:UInt. (f * (fun n:UInt { 1 }))(m) = f(m) by {
    arbitrary m:UInt
    expand operator*.
  }
  apply bigo_pointwise_eq[f * (fun n:UInt { 1 }), f] to pointwise
end

// Pointwise multiplication distributes over pointwise addition up to ≈.
theorem bigo_dist: all f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt.
  f * (g + h) ≈ f * g + f * h
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt
  have pointwise: all m:UInt. (f * (g + h))(m) = (f * g + f * h)(m) by {
    arbitrary m:UInt
    expand operator+ | operator*
    show f(m) * (g(m) + h(m)) = f(m) * g(m) + f(m) * h(m)
    uint_dist_mult_add
  }
  apply bigo_pointwise_eq[f * (g + h), f * g + f * h] to pointwise
end

// Two-sided sum absorption: a dominated summand can be dropped under ≈.
theorem bigo_add_dominated_absorb_equiv: all f:fn UInt->UInt, g:fn UInt->UInt.
  if g ≲ f then f + g ≈ f
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume g_f: g ≲ f
  expand operator≈
  have A: f + g ≲ f by apply bigo_add_absorb to g_f
  have B: f ≲ f + g by bigo_self_le_add
  A, B
end

// A positive constant factor drops out of ≈.
theorem bigo_const_mult_equiv: all f:fn UInt->UInt, k:UInt.
  if 0 < k then k * f ≈ f
proof
  arbitrary f:fn UInt->UInt, k:UInt
  assume k_pos: 0 < k
  expand operator≈
  have A: k * f ≲ f by bigo_const_mult
  have k_ge_1: 1 ≤ k by apply uint_pos_implies_one_le to k_pos
  have B: f ≲ k * f by apply bigo_le_const_mult[f, k] to k_ge_1
  A, B
end

// Pointwise maximum of cost functions.
fun max (f : fn UInt -> UInt, g : fn UInt -> UInt) {
  fun n:UInt { max(f(n), g(n)) }
}

// The pointwise max is bounded above by the pointwise sum.
theorem bigo_max_le_add: all f:fn UInt->UInt, g:fn UInt->UInt.
  max(f, g) ≲ f + g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≲ | operator+ | max
  choose 0, 1
  arbitrary n:UInt
  assume _
  show max(f(n), g(n)) ≤ 1 * (f(n) + g(n))
  have f_le: f(n) ≤ f(n) + g(n) by uint_less_equal_add
  have g_le: g(n) ≤ f(n) + g(n) by uint_less_equal_add_left
  apply uint_max_less_equal to f_le, g_le
end

// The pointwise sum is bounded by a constant multiple of the pointwise max.
theorem bigo_add_le_max: all f:fn UInt->UInt, g:fn UInt->UInt.
  f + g ≲ max(f, g)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  expand operator≲ | operator+ | max
  choose 0, 2
  arbitrary n:UInt
  assume _
  show f(n) + g(n) ≤ 2 * max(f(n), g(n))
  have f_le: f(n) ≤ max(f(n), g(n)) by uint_max_greater_left
  have g_le: g(n) ≤ max(f(n), g(n)) by uint_max_greater_right
  have sum_le: f(n) + g(n) ≤ max(f(n), g(n)) + max(f(n), g(n))
    by apply uint_add_mono_less_equal to f_le, g_le
  replace uint_two_mult[max(f(n), g(n))]
  sum_le
end

// Big-Omega: `bigo_omega(f, g)` means `f` asymptotically dominates `g`
// — equivalently, `g ≲ f`. Big-Omega is the dual of the `≲` (Big-O) preorder.
fun bigo_omega(f : fn UInt -> UInt, g : fn UInt -> UInt) {
  g ≲ f
}

// Big-Omega is reflexive.
theorem bigo_omega_refl: all f:fn UInt->UInt. bigo_omega(f, f)
proof
  arbitrary f:fn UInt->UInt
  expand bigo_omega
  bigo_refl
end

// Big-Omega is transitive.
theorem bigo_omega_trans:
  all f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt.
  if bigo_omega(f, g) and bigo_omega(g, h) then bigo_omega(f, h)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt, h:fn UInt->UInt
  assume prem
  have gf: g ≲ f by expand bigo_omega in prem
  have hg: h ≲ g by expand bigo_omega in prem
  expand bigo_omega
  apply bigo_trans to hg, gf
end

// Asymptotic equivalence is exactly Big-Theta: `f ≈ g` iff `f` is both
// Big-O and Big-Omega of `g`.
theorem bigo_equiv_iff_theta: all f:fn UInt->UInt, g:fn UInt->UInt.
  f ≈ g ⇔ (f ≲ g and bigo_omega(f, g))
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  have fwd: if f ≈ g then (f ≲ g and bigo_omega(f, g)) by {
    assume H
    have fg: f ≲ g by expand operator≈ in H
    have gf: g ≲ f by expand operator≈ in H
    have go: bigo_omega(f, g) by { expand bigo_omega gf }
    fg, go
  }
  have bkwd: if (f ≲ g and bigo_omega(f, g)) then f ≈ g by {
    assume H
    have fg: f ≲ g by H
    have gf: g ≲ f by expand bigo_omega in H
    expand operator≈
    fg, gf
  }
  fwd, bkwd
end

// Little-o: `bigo_little_o(f, g)` recasts the standard ε-formulation
// `lim f/g = 0` to the `UInt` setting. As `ε` shrinks toward `0`, its
// reciprocal `c = 1/ε` grows without bound, so the condition
// `f(n) < ε * g(n)` becomes `c * f(n) < g(n)` — eventually true for every
// positive `UInt` constant `c`. Spelled as a named function rather than an
// operator because no `≪` token is wired into the grammar.
fun bigo_little_o(f : fn UInt -> UInt, g : fn UInt -> UInt) {
  all c:UInt. if 0 < c then some n0:UInt. all n:UInt. if n0 ≤ n then c * f(n) < g(n)
}

// Little-omega: the strict cousin of Big-Omega and the dual of little-o.
// `bigo_little_omega(f, g)` says `f` strictly dominates `g`, i.e. little-o
// the other way round.
fun bigo_little_omega(f : fn UInt -> UInt, g : fn UInt -> UInt) {
  bigo_little_o(g, f)
}

// Little-o implies Big-O: strict eventual domination is stronger than
// constant-factor eventual domination.
theorem bigo_little_implies_big: all f:fn UInt->UInt, g:fn UInt->UInt.
  if bigo_little_o(f, g) then f ≲ g
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H: bigo_little_o(f, g)
  have one_pos: (0:UInt) < 1 by .
  have step1: some n0:UInt. all n:UInt. if n0 ≤ n then 1 * f(n) < g(n)
    by apply (expand bigo_little_o in H)[1] to one_pos
  obtain n0 where step: all n:UInt. if n0 ≤ n then 1 * f(n) < g(n) from step1
  expand operator≲
  choose n0, 1
  arbitrary n:UInt
  assume n0_n: n0 ≤ n
  show f(n) ≤ 1 * g(n)
  have lt: f(n) < g(n) by apply step to n0_n
  apply uint_less_implies_less_equal to lt
end

// Little-o is irreflexive: no function strictly dominates itself.
// Instantiating the `c = 1` case at `n = n0` would force `f(n0) < f(n0)`.
theorem bigo_little_irrefl: all f:fn UInt->UInt. not bigo_little_o(f, f)
proof
  arbitrary f:fn UInt->UInt
  assume H: bigo_little_o(f, f)
  have one_pos: (0:UInt) < 1 by .
  have step1: some n0:UInt. all n:UInt. if n0 ≤ n then 1 * f(n) < f(n)
    by apply (expand bigo_little_o in H)[1] to one_pos
  obtain n0 where step: all n:UInt. if n0 ≤ n then 1 * f(n) < f(n) from step1
  have n0_n0: n0 ≤ n0 by .
  have lt: f(n0) < f(n0) by apply step to n0_n0
  apply uint_less_irreflexive to lt
end

// Little-omega unfolds to a swapped little-o.
theorem bigo_little_omega_swap: all f:fn UInt->UInt, g:fn UInt->UInt.
  if bigo_little_omega(f, g) then bigo_little_o(g, f)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H
  expand bigo_little_omega in H
end

// Little-omega is irreflexive, by symmetry with little-o.
theorem bigo_little_omega_irrefl: all f:fn UInt->UInt. not bigo_little_omega(f, f)
proof
  arbitrary f:fn UInt->UInt
  assume H: bigo_little_omega(f, f)
  have ff: bigo_little_o(f, f) by expand bigo_little_omega in H
  apply bigo_little_irrefl to ff
end

// Little-omega implies Big-Omega.
theorem bigo_little_omega_implies_big_omega: all f:fn UInt->UInt, g:fn UInt->UInt.
  if bigo_little_omega(f, g) then bigo_omega(f, g)
proof
  arbitrary f:fn UInt->UInt, g:fn UInt->UInt
  assume H: bigo_little_omega(f, g)
  have gf: bigo_little_o(g, f) by expand bigo_little_omega in H
  have gf_big: g ≲ f by apply bigo_little_implies_big to gf
  expand bigo_omega
  gf_big
end

// Linearithmic time: n * log(n).
fun O_n_log_n(n:UInt) { n * log(n) }

// Cubic time.
fun O_n3(n:UInt) { n * n * n }

// Exponential time: 2^n.
fun O_2pow_n(n:UInt) { 2 ^ n }

// Linear is bounded by linearithmic: for n ≥ 2, log(n) ≥ 1, so
// n ≤ n * log(n).
theorem bigo_linear_le_n_log_n: O_n ≲ O_n_log_n
proof
  expand operator≲ | O_n | O_n_log_n
  choose 2, 1
  arbitrary n:UInt
  assume two_n: 2 ≤ n
  show n ≤ 1 * (n * log(n))
  have one_log: 1 ≤ log(n) by apply uint_log_greater_one to two_n
  apply uint_mult_mono_le[n] to one_log
end

// Linearithmic is bounded by quadratic: log(n) ≤ n, so n * log(n) ≤ n * n.
theorem bigo_n_log_n_le_quadratic: O_n_log_n ≲ O_n2
proof
  expand operator≲ | O_n_log_n | O_n2
  choose 0, 1
  arbitrary n:UInt
  assume _
  show n * log(n) ≤ 1 * (n * n)
  have logn_n: log(n) ≤ n by uint_logn_le_n
  have n_n: n ≤ n by .
  conclude n * log(n) ≤ 1 * (n * n) by apply uint_mult_mono_le2 to n_n, logn_n
end

// Quadratic is bounded by cubic: for n ≥ 1, n * n ≤ n * n * n.
theorem bigo_quadratic_le_cubic: O_n2 ≲ O_n3
proof
  expand operator≲ | O_n2 | O_n3
  choose 1, 1
  arbitrary n:UInt
  assume one_n: 1 ≤ n
  show n * n ≤ 1 * (n * n * n)
  apply uint_mult_mono_le[n * n] to one_n
end

// Linear is bounded by exponential: for n ≥ 1, n < 2^(1+log(n)) ≤ 2^(1+n) = 2 * 2^n.
theorem bigo_linear_le_2pow_n: O_n ≲ O_2pow_n
proof
  expand operator≲ | O_n | O_2pow_n
  choose 1, 2
  arbitrary n:UInt
  assume one_n: 1 ≤ n
  show n ≤ 2 * 2^n
  have n_pos: 0 < n by replace uint_less_is_less_equal[0, n] one_n
  have lt: n < 2^(1 + log(n)) by apply less_pow_log to n_pos
  have logn_n: log(n) ≤ n by uint_logn_le_n
  have one_le: (1:UInt) ≤ 1 by .
  have step: 1 + log(n) ≤ 1 + n by apply uint_add_mono_less_equal to one_le, logn_n
  have one_le_two: (1:UInt) ≤ 2 by .
  have pow_step: 2^(1 + log(n)) ≤ 2^(1 + n)
    by apply (apply uint_pow_le_mono_r[1 + n, 2, 1 + log(n)] to one_le_two) to step
  have lt_le: n < 2^(1 + n) by {
    have or_eq: 2^(1 + log(n)) < 2^(1 + n) or 2^(1 + log(n)) = 2^(1 + n) by expand operator≤ in pow_step
    cases or_eq
    case lt_case { apply uint_less_trans to lt, lt_case }
    case eq_case { replace eq_case in lt }
  }
  have expand_pow: 2^(1 + n) = 2 * 2^n by uint_pow_add_r[2, 1, n]
  have lt_le2: n < 2 * 2^n by replace expand_pow in lt_le
  apply uint_less_implies_less_equal to lt_le2
end

// Polynomial monotonicity in the exponent. For n ≥ 1, n^a ≤ n^b when a ≤ b.
// The threshold n0 = 1 is enough: 0^a is 0 (when a > 0) or 1 (when a = 0),
// so the n = 0 corner is excluded here for simplicity.
theorem bigo_pow_mono: all a:UInt, b:UInt.
  if a ≤ b then (fun n:UInt { n^a }) ≲ (fun n:UInt { n^b })
proof
  arbitrary a:UInt, b:UInt
  assume a_le_b: a ≤ b
  expand operator≲
  choose 1, 1
  arbitrary n:UInt
  assume one_n: 1 ≤ n
  show n^a ≤ 1 * n^b
  apply (apply uint_pow_le_mono_r[b, n, a] to one_n) to a_le_b
end

// Pointwise: `log(f)(n) = log(f(n)) ≤ f(n)` by `uint_logn_le_n`.
// Hence `log(f) ≲ f` for any cost function `f`.
theorem bigo_log_le_self: all f:fn UInt->UInt. log(f) ≲ f
proof
  arbitrary f:fn UInt->UInt
  expand operator≲ | log
  choose 0, 1
  arbitrary n:UInt
  assume _
  show log(f(n)) ≤ 1 * f(n)
  uint_logn_le_n
end

// Log of a constant function is bounded: `log(O_1) ≲ O_1`.
// Instance of `bigo_log_le_self` at `f = O_1`.
theorem bigo_log_const: log(O_1) ≲ O_1
proof
  bigo_log_le_self[O_1]
end

// Iterated log is bounded by log: `log(O_log) ≲ O_log`.
// Instance of `bigo_log_le_self` at `f = O_log`; concretely
// `log(log(n)) ≤ log(n)` for every `n`, which is the
// `n_log_log(n) ≤ log(n)` step in the `O(n log log n)` discussion.
theorem bigo_log_log: log(O_log) ≲ O_log
proof
  bigo_log_le_self[O_log]
end

// Polynomial-vs-exponential domination, base case k = 2: n*n ≤ 2^n for n ≥ 4.
// Proven by k-induction starting at 4. The inductive step uses the polynomial
// slack 1 + 2m ≤ m*m (via 1 + 2m ≤ 4m ≤ m*m, both valid for m ≥ 4) to bound
// (1+m)*(1+m) = 1 + 2m + m*m ≤ 2 * m*m, then folds the IH m*m ≤ 2^m through a
// factor of 2 to land on 2^(1+m).
lemma uint_quad_le_2pow: all n:UInt. if 4 ≤ n then n * n ≤ 2 ^ n
proof
  define P = fun n:UInt { n * n ≤ 2 ^ n }
  have base: P(4) by {
    expand P
    show 4 * 4 ≤ 2 ^ 4
    .
  }
  have ind: all m:UInt. if 4 ≤ m and P(m) then P(1 + m) by {
    arbitrary m:UInt
    assume prem
    have m_ge_4: 4 ≤ m by prem
    have IH: m * m ≤ 2 ^ m by expand P in prem
    expand P
    show (1 + m) * (1 + m) ≤ 2 ^ (1 + m)

    have expand_sq: (1 + m) * (1 + m) = 1 + 2 * m + m * m by {
      replace uint_dist_mult_add_right[1, m, 1+m]
           | uint_dist_mult_add[m, 1, m]
           | uint_two_mult[m].
    }

    have m_ge_1: 1 ≤ m by {
      have one_le_four: (1:UInt) ≤ 4 by .
      apply uint_less_equal_trans to one_le_four, m_ge_4
    }

    have m_le_m: m ≤ m by .
    have four_m_le_m_m: 4 * m ≤ m * m
      by apply uint_mult_mono_le2 to m_ge_4, m_le_m

    have one_le_2m: (1:UInt) ≤ 2 * m by {
      have one_le_two: (1:UInt) ≤ 2 by .
      have two_le_2m: (2:UInt) ≤ 2 * m by apply uint_mult_mono_le[2] to m_ge_1
      apply uint_less_equal_trans to one_le_two, two_le_2m
    }

    have four_m_eq: (4:UInt) * m = 2 * m + 2 * m
      by uint_dist_mult_add_right[2, 2, m]

    have step_2m_le_4m: 1 + 2 * m ≤ 4 * m by {
      replace four_m_eq
      have two_m_le: 2 * m ≤ 2 * m by .
      apply uint_add_mono_less_equal to one_le_2m, two_m_le
    }

    have slack: 1 + 2 * m ≤ m * m
      by apply uint_less_equal_trans to step_2m_le_4m, four_m_le_m_m

    have step_sum: (1 + 2 * m) + m * m ≤ m * m + m * m by {
      have mm_le_mm: m * m ≤ m * m by .
      apply uint_add_mono_less_equal to slack, mm_le_mm
    }

    have two_mm_eq: m * m + m * m = 2 * (m * m)
      by symmetric uint_two_mult[m * m]
    have step_2mm: (1 + 2 * m) + m * m ≤ 2 * (m * m)
      by replace two_mm_eq in step_sum

    have step_lhs_2mm: (1 + m) * (1 + m) ≤ 2 * (m * m) by {
      replace expand_sq
      step_2mm
    }

    have step_two_pow_m: 2 * (m * m) ≤ 2 * 2 ^ m
      by apply uint_mult_mono_le[2] to IH

    have step_chain: (1 + m) * (1 + m) ≤ 2 * 2 ^ m
      by apply uint_less_equal_trans to step_lhs_2mm, step_two_pow_m

    have pow_step: 2 ^ (1 + m) = 2 * 2 ^ m by uint_pow_add_r[2, 1, m]

    replace pow_step
    step_chain
  }
  expand P in apply uint_k_induction[P, 4] to base, ind
end

// Quadratic is bounded by exponential: O(n^2) ≲ O(2^n). Threshold n0 = 4,
// constant c = 1 (uint_quad_le_2pow gives the pointwise inequality directly).
theorem bigo_quadratic_le_2pow_n: O_n2 ≲ O_2pow_n
proof
  expand operator≲ | O_n2 | O_2pow_n
  choose 4, 1
  arbitrary n:UInt
  assume four_n: 4 ≤ n
  show n * n ≤ 1 * 2 ^ n
  apply uint_quad_le_2pow to four_n
end

// Polynomial-vs-exponential domination, k = 3: n*n*n ≤ 2^n for n ≥ 10.
// Proven by k-induction starting at 10 (base 10^3 = 1000 ≤ 1024 = 2^10).
// In the inductive step (1+m)^3 expands to 1 + 3m + 3*m*m + m*m*m; the
// polynomial slack 1 + 3m + 3*m*m ≤ m*m*m holds for m ≥ 4 (and so for
// m ≥ 10), giving (1+m)^3 ≤ 2 * m*m*m and folding the IH through a factor
// of 2 to land on 2^(1+m).
lemma uint_cube_le_2pow: all n:UInt. if 10 ≤ n then n * n * n ≤ 2 ^ n
proof
  define P = fun n:UInt { n * n * n ≤ 2 ^ n }
  have base: P(10) by {
    expand P
    show 10 * 10 * 10 ≤ 2 ^ 10
    .
  }
  have ind: all m:UInt. if 10 ≤ m and P(m) then P(1 + m) by {
    arbitrary m:UInt
    assume prem
    have m_ge_10: 10 ≤ m by prem
    have IH: m * m * m ≤ 2 ^ m by expand P in prem
    expand P
    show (1 + m) * (1 + m) * (1 + m) ≤ 2 ^ (1 + m)

    have m_ge_4: 4 ≤ m by {
      have four_le_ten: (4:UInt) ≤ 10 by .
      apply uint_less_equal_trans to four_le_ten, m_ge_10
    }
    have m_ge_1: 1 ≤ m by {
      have one_le_four: (1:UInt) ≤ 4 by .
      apply uint_less_equal_trans to one_le_four, m_ge_4
    }
    have m_le_m: m ≤ m by .

    have expand_sq: (1 + m) * (1 + m) = 1 + 2 * m + m * m by {
      replace uint_dist_mult_add_right[1, m, 1+m]
           | uint_dist_mult_add[m, 1, m]
           | uint_two_mult[m].
    }
    have step1: (1 + m) * (1 + m) * (1 + m) = (1 + 2*m + m*m) * (1 + m)
      by replace expand_sq.
    have step2: (1 + 2*m + m*m) * (1 + m) = (1 + 2*m + m*m) + (1 + 2*m + m*m) * m
      by uint_dist_mult_add[1 + 2*m + m*m, 1, m]
    have step3: (1 + 2*m + m*m) * m = m + 2*m*m + m*m*m by {
      replace uint_dist_mult_add_right[1, 2*m + m*m, m]
           | uint_dist_mult_add_right[2*m, m*m, m].
    }
    have step4: (1 + m) * (1 + m) * (1 + m)
              = 1 + 2*m + m*m + m + 2*m*m + m*m*m by {
      replace step1 | step2 | step3.
    }
    // Regroup to the standard form 1 + 3*m + 3*m*m + m*m*m.
    have regroup: 1 + 2*m + m*m + m + 2*m*m + m*m*m = 1 + 3*m + 3*m*m + m*m*m by {
      equations
            1 + 2*m + m*m + m + 2*m*m + m*m*m
          = 1 + 2*m + m + m*m + 2*m*m + m*m*m   by replace uint_add_commute[m*m, m].
      ... = 1 + (2*m + m) + (m*m + 2*m*m) + m*m*m   by .
      ... = 1 + 3*m + (m*m + 2*m*m) + m*m*m   by {
              have e: 2*m + m = 3*m by symmetric uint_dist_mult_add_right[2, 1, m]
              replace e.
            }
      ... = 1 + 3*m + 3*m*m + m*m*m   by {
              have ee: 1 * m * m + 2 * m * m = (1 + 2) * m * m
                by symmetric uint_dist_mult_add_right[1, 2, m*m]
              replace ee.
            }
    }
    have step5: (1 + m) * (1 + m) * (1 + m) = 1 + 3*m + 3*m*m + m*m*m
      by transitive step4 regroup

    // Polynomial slack: 1 + 3*m + 3*m*m ≤ m*m*m for m ≥ 4.
    // 1 + 3*m ≤ 4*m (via 1 ≤ m) ≤ m*m (via 4 ≤ m).
    have step_A: 1 + 3 * m ≤ 4 * m by {
      have three_m_le: 3 * m ≤ 3 * m by .
      have rev: 1 + 3 * m ≤ m + 3 * m by apply uint_add_mono_less_equal to m_ge_1, three_m_le
      have e: m + 3 * m = 4 * m by {
        have hh: (1 + 3) * m = 1 * m + 3 * m by uint_dist_mult_add_right[1, 3, m]
        replace hh.
      }
      replace e in rev
    }
    have step_B: 4 * m ≤ m * m by apply uint_mult_mono_le2 to m_ge_4, m_le_m
    have step_C: 1 + 3 * m ≤ m * m by apply uint_less_equal_trans to step_A, step_B
    // (1 + 3*m) + 3*m*m ≤ m*m + 3*m*m.
    have three_mm_le: 3 * m * m ≤ 3 * m * m by .
    have step_D_sum: (1 + 3 * m) + 3 * m * m ≤ m * m + 3 * m * m
      by apply uint_add_mono_less_equal to step_C, three_mm_le
    // m*m + 3*m*m ≤ m*m*m via (m + 3*m)*m: distrib m + 3m ≤ m*m, multiply by m.
    have e_4m: m + 3 * m = 4 * m by {
      have hh: (1 + 3) * m = 1 * m + 3 * m by uint_dist_mult_add_right[1, 3, m]
      replace hh.
    }
    have step_m3m_le_mm: m + 3 * m ≤ m * m by replace e_4m step_B
    have step_dist_m: (m + 3 * m) * m ≤ m * m * m
      by apply uint_mult_mono_le2 to step_m3m_le_mm, m_le_m
    have dist_3mm: (m + 3 * m) * m = m * m + 3 * m * m
      by uint_dist_mult_add_right[m, 3 * m, m]
    have step_mm3mm_le_mmm: m * m + 3 * m * m ≤ m * m * m
      by replace dist_3mm in step_dist_m
    // Compose.
    have step_F: (1 + 3 * m) + 3 * m * m ≤ m * m * m
      by apply uint_less_equal_trans to step_D_sum, step_mm3mm_le_mmm

    // (1 + 3*m + 3*m*m) + m*m*m ≤ m*m*m + m*m*m = 2 * (m*m*m).
    have mmm_le_mmm: m * m * m ≤ m * m * m by .
    have step_sum_full: ((1 + 3 * m) + 3 * m * m) + m * m * m ≤ m * m * m + m * m * m
      by apply uint_add_mono_less_equal to step_F, mmm_le_mmm
    have two_mmm_eq: 2 * (m * m * m) = m * m * m + m * m * m
      by uint_two_mult[m * m * m]

    have step_lhs_2mmm: (1 + m) * (1 + m) * (1 + m) ≤ 2 * (m * m * m) by {
      replace step5
      replace two_mmm_eq
      step_sum_full
    }
    have step_two_pow_m: 2 * (m * m * m) ≤ 2 * 2 ^ m
      by apply uint_mult_mono_le[2] to IH
    have step_chain: (1 + m) * (1 + m) * (1 + m) ≤ 2 * 2 ^ m
      by apply uint_less_equal_trans to step_lhs_2mmm, step_two_pow_m
    have pow_step: 2 ^ (1 + m) = 2 * 2 ^ m by uint_pow_add_r[2, 1, m]
    replace pow_step
    step_chain
  }
  expand P in apply uint_k_induction[P, 10] to base, ind
end

// Cubic is bounded by exponential: O(n^3) ≲ O(2^n). Threshold n0 = 10,
// constant c = 1 (uint_cube_le_2pow gives the pointwise inequality directly).
theorem bigo_cubic_le_2pow_n: O_n3 ≲ O_2pow_n
proof
  expand operator≲ | O_n3 | O_2pow_n
  choose 10, 1
  arbitrary n:UInt
  assume ten_n: 10 ≤ n
  show n * n * n ≤ 1 * 2 ^ n
  apply uint_cube_le_2pow to ten_n
end

// Pointwise bound: for `k ≥ 1`, `log(n^k) ≤ k * (1 + log(n))`. Used by
// `bigo_log_pow`. Proof outline: when `n > 0`, `n ≤ 2^(1 + log(n))` by
// `less_pow_log`, so `n^k ≤ (2^(1 + log(n)))^k = 2^((1 + log(n)) * k)`,
// hence `log(n^k) ≤ (1 + log(n)) * k`. The `n = 0` case folds into the
// trivial `0 ≤ k * (1 + log(0))`.
lemma uint_log_pow_le: all n:UInt, k:UInt.
  if 1 ≤ k then log(n^k) ≤ k * (1 + log(n))
proof
  arbitrary n:UInt, k:UInt
  assume one_le_k: 1 ≤ k
  have k_pos: 0 < k by replace uint_less_is_less_equal[0, k] one_le_k
  cases uint_zero_or_positive[n]
  case n_zero: n = 0 {
    have zk: (0:UInt)^k = 0 by apply uint_zero_pow to k_pos
    replace n_zero | zk
    show log((0:UInt)) ≤ k * (1 + log((0:UInt)))
    uint_zero_le
  }
  case n_pos: 0 < n {
    have n_lt: n < 2^(1 + log(n)) by apply less_pow_log to n_pos
    have n_le: n ≤ 2^(1 + log(n)) by apply uint_less_implies_less_equal to n_lt
    have step_pow: n^k ≤ (2^(1 + log(n)))^k
      by apply uint_pow_le_mono_l[k, n, 2^(1 + log(n))] to n_le
    have flat_pow: (2^(1 + log(n)))^k = 2^((1 + log(n)) * k)
      by uint_pow_mul_r[2, 1 + log(n), k]
    have step_pow2: n^k ≤ 2^((1 + log(n)) * k)
      by replace flat_pow in step_pow
    have step_log: log(n^k) ≤ log(2^((1 + log(n)) * k))
      by apply uint_log_mono to step_pow2
    have log_simp: log(2^((1 + log(n)) * k)) = (1 + log(n)) * k by log_pow
    have step_final: log(n^k) ≤ (1 + log(n)) * k
      by replace log_simp in step_log
    show log(n^k) ≤ k * (1 + log(n))
    replace uint_mult_commute[k, 1 + log(n)]
    step_final
  }
end

// Asymptotic log-of-power: for fixed exponent `k ≥ 1`, the cost function
// `fun n. log(n^k)` is asymptotically equivalent to `log(O_n) = fun n. log(n)`.
// Concretely `log(n^k)` lies between `log(n)` and `k * (1 + log(n))`, and the
// constant factor `k` drops under `≈` — change of base for powers is invisible
// in big-Theta.
theorem bigo_log_pow: all k:UInt.
  if 1 ≤ k then log((fun n:UInt { n^k })) ≈ log(O_n)
proof
  arbitrary k:UInt
  assume one_le_k: 1 ≤ k
  expand operator≈
  have upper: log((fun n:UInt { n^k })) ≲ log(O_n) by {
    expand operator≲ | log | O_n
    choose 2, 2 * k
    arbitrary n:UInt
    assume two_n: 2 ≤ n
    show log(n^k) ≤ 2 * k * log(n)
    have bound: log(n^k) ≤ k * (1 + log(n))
      by apply uint_log_pow_le[n, k] to one_le_k
    have dist: k * (1 + log(n)) = k + k * log(n)
      by uint_dist_mult_add[k, 1, log(n)]
    have bound2: log(n^k) ≤ k + k * log(n) by replace dist in bound
    have one_logn: 1 ≤ log(n) by apply uint_log_greater_one to two_n
    have k_le_klog: k ≤ k * log(n) by {
      have h: k * 1 ≤ k * log(n) by apply uint_mult_mono_le[k] to one_logn
      h
    }
    have klog_le: k * log(n) ≤ k * log(n) by .
    have sum_le: k + k * log(n) ≤ k * log(n) + k * log(n)
      by apply uint_add_mono_less_equal to k_le_klog, klog_le
    have klog_klog_eq: k * log(n) + k * log(n) = 2 * k * log(n) by {
      have assoc_eq: 2 * (k * log(n)) = 2 * k * log(n)
        by symmetric uint_mult_assoc[2, k, log(n)]
      replace symmetric uint_two_mult[k * log(n)]
      assoc_eq
    }
    have sum_le2: k + k * log(n) ≤ 2 * k * log(n)
      by replace klog_klog_eq in sum_le
    apply uint_less_equal_trans to bound2, sum_le2
  }
  have lower: log(O_n) ≲ log((fun n:UInt { n^k })) by {
    expand operator≲ | log | O_n
    choose 1, 1
    arbitrary n:UInt
    assume one_n: 1 ≤ n
    show log(n) ≤ 1 * log(n^k)
    have n_le: n ≤ n^k
      by apply (apply uint_pow_le_mono_r[k, n, 1] to one_n) to one_le_k
    have log_le: log(n) ≤ log(n^k) by apply uint_log_mono to n_le
    log_le
  }
  upper, lower
end

// Log of a power is bounded by log: for `k ≥ 1`, `log((fun n. n^k)) ≲ log(O_n)`.
// One direction of `bigo_log_pow`; spelled out separately because callers often
// only need the upper bound (a `log(n^k)` factor in a complexity expression
// collapses to `log(n)` for asymptotic purposes).
theorem bigo_log_pow_le: all k:UInt.
  if 1 ≤ k then log((fun n:UInt { n^k })) ≲ log(O_n)
proof
  arbitrary k:UInt
  assume one_le_k: 1 ≤ k
  have eq: log((fun n:UInt { n^k })) ≈ log(O_n)
    by apply bigo_log_pow[k] to one_le_k
  expand operator≈ in eq
end

// Strict (little-o) form of `bigo_pow_mono`: for `a < b`, `n^a` is little-o
// of `n^b`, i.e. for any constant `c > 0`, eventually `c * n^a < n^b`.
// Threshold `n0 = 1 + c`, factor `n^b = n^a * n^(b ∸ a)` via `a + (b ∸ a) = b`
// and `uint_pow_add_r`; with `b ∸ a ≥ 1` and `1 ≤ n`, `n^(b ∸ a) ≥ n > c`,
// then multiply through by `n^a > 0`.
theorem bigo_pow_strict_mono: all a:UInt, b:UInt.
  if a < b then bigo_little_o(fun n:UInt {n^a}, fun n:UInt {n^b})
proof
  arbitrary a:UInt, b:UInt
  assume a_lt_b
  have a_le_b: a ≤ b by apply uint_less_implies_less_equal to a_lt_b
  have ba_id: a + (b ∸ a) = b by apply uint_monus_add_identity[b, a] to a_le_b
  have ba_ge_1: 1 ≤ b ∸ a by {
    have one_plus_a_le_b: 1 + a ≤ b by replace uint_less_is_less_equal in a_lt_b
    have shaped: a + 1 ≤ b by replace uint_add_commute[1, a] in one_plus_a_le_b
    replace symmetric ba_id in shaped
  }
  expand bigo_little_o
  arbitrary c:UInt
  assume _c_pos
  choose 1 + c
  arbitrary n:UInt
  assume n_ge: 1 + c ≤ n
  show c * n^a < n^b
  have one_le_n: 1 ≤ n by {
    have h: (1:UInt) ≤ 1 + c by uint_less_equal_add
    apply uint_less_equal_trans to h, n_ge
  }
  have n_pos: 0 < n by replace uint_less_is_less_equal[0, n] one_le_n
  have na_pos: 0 < n^a by apply uint_pow_pos[n, a] to n_pos
  have c_lt_n: c < n by replace uint_less_is_less_equal[c, n] n_ge
  have n_le_nba: n ≤ n^(b ∸ a)
    by apply (apply uint_pow_le_mono_r[b ∸ a, n, 1] to one_le_n) to ba_ge_1
  have c_lt_nba: c < n^(b ∸ a) by {
    have or_n: n < n^(b ∸ a) or n = n^(b ∸ a) by expand operator≤ in n_le_nba
    cases or_n
    case lt { apply uint_less_trans to c_lt_n, lt }
    case eq: n = n^(b ∸ a) { replace symmetric eq c_lt_n }
  }
  have mult_step: n^a * c < n^a * n^(b ∸ a)
    by apply uint_pos_mult_both_sides_of_less to na_pos, c_lt_nba
  have pow_factor: n^b = n^a * n^(b ∸ a) by {
    replace symmetric ba_id
    uint_pow_add_r[n, a, b ∸ a]
  }
  replace pow_factor
  replace uint_mult_commute[c, n^a]
  mult_step
end

// Polynomial closure, degree 1: a degree-1 polynomial with positive leading
// coefficient is asymptotically equivalent to its leading monomial.
// `a*n + b ≈ n` when `1 ≤ a`. Upper bound at `n0 = 1`, `c = a + b`: the
// constant term `b` is absorbed since `b ≤ b*n` for `n ≥ 1`. Lower bound at
// `n0 = 0`, `c = 1`: `1 ≤ a` gives `n ≤ a*n ≤ a*n + b` pointwise.
theorem bigo_linear_closure: all a:UInt, b:UInt.
  if 1 ≤ a then (fun n:UInt { a * n + b }) ≈ (fun n:UInt { n })
proof
  arbitrary a:UInt, b:UInt
  assume a_pos: 1 ≤ a
  expand operator≈
  have upper: (fun n:UInt { a * n + b }) ≲ (fun n:UInt { n }) by {
    expand operator≲
    choose 1, a + b
    arbitrary n:UInt
    assume n_ge_1: 1 ≤ n
    show a * n + b ≤ (a + b) * n
    have b_le_bn: b ≤ b * n by apply uint_mult_mono_le[b, 1, n] to n_ge_1
    have an_le: a * n ≤ a * n by .
    have sum_le: a * n + b ≤ a * n + b * n
      by apply uint_add_mono_less_equal to an_le, b_le_bn
    have expand_eq: (a + b) * n = a * n + b * n by uint_dist_mult_add_right
    replace expand_eq
    sum_le
  }
  have lower: (fun n:UInt { n }) ≲ (fun n:UInt { a * n + b }) by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show n ≤ 1 * (a * n + b)
    have n_le_n: n ≤ n by .
    have n_le_an: n ≤ a * n
      by apply uint_mult_mono_le2[1, n, a, n] to a_pos, n_le_n
    have an_le_anb: a * n ≤ a * n + b by uint_less_equal_add
    apply uint_less_equal_trans to n_le_an, an_le_anb
  }
  upper, lower
end

// Polynomial closure, degree 2: a degree-2 polynomial with positive leading
// coefficient is asymptotically equivalent to its leading monomial.
// `a*n*n + b*n + c ≈ n*n` when `1 ≤ a`. Upper bound at `n0 = 1`,
// `c0 = a + b + c`: the lower-order terms `b*n` and `c` are absorbed since
// `b*n ≤ b*(n*n)` and `c ≤ c*(n*n)` for `n ≥ 1`. Lower bound at `n0 = 0`,
// `c0 = 1`: `1 ≤ a` gives `n*n ≤ a*(n*n) ≤ a*(n*n) + (b*n + c)` pointwise.
theorem bigo_quadratic_closure: all a:UInt, b:UInt, c:UInt.
  if 1 ≤ a then (fun n:UInt { a * n * n + b * n + c }) ≈ (fun n:UInt { n * n })
proof
  arbitrary a:UInt, b:UInt, c:UInt
  assume a_pos: 1 ≤ a
  expand operator≈
  have upper: (fun n:UInt { a * n * n + b * n + c }) ≲ (fun n:UInt { n * n }) by {
    expand operator≲
    choose 1, a + b + c
    arbitrary n:UInt
    assume n_ge_1: 1 ≤ n
    show a * n * n + b * n + c ≤ (a + b + c) * (n * n)
    have n_le_n: n ≤ n by .
    have n_le_nn: n ≤ n * n
      by apply uint_mult_mono_le2[1, n, n, n] to n_ge_1, n_le_n
    have one_le_nn: 1 ≤ n * n by apply uint_less_equal_trans to n_ge_1, n_le_nn
    have bn_le_bnn: b * n ≤ b * (n * n) by apply uint_mult_mono_le[b, n, n*n] to n_le_nn
    have c_le_cnn: c ≤ c * (n * n) by apply uint_mult_mono_le[c, 1, n*n] to one_le_nn
    have ann_le: a * n * n ≤ a * (n * n) by .
    have sum1: a * n * n + b * n ≤ a * (n * n) + b * (n * n)
      by apply uint_add_mono_less_equal to ann_le, bn_le_bnn
    have sum2: a * n * n + b * n + c ≤ a * (n * n) + b * (n * n) + c * (n * n)
      by apply uint_add_mono_less_equal to sum1, c_le_cnn
    have expand_eq: (a + b + c) * (n * n) = a * (n * n) + b * (n * n) + c * (n * n) by {
      have step1: (a + b + c) * (n * n) = (a + b) * (n * n) + c * (n * n)
        by uint_dist_mult_add_right[a + b, c, n * n]
      have step2: (a + b) * (n * n) = a * (n * n) + b * (n * n)
        by uint_dist_mult_add_right[a, b, n * n]
      replace step1 | step2.
    }
    replace expand_eq
    sum2
  }
  have lower: (fun n:UInt { n * n }) ≲ (fun n:UInt { a * n * n + b * n + c }) by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show n * n ≤ 1 * (a * n * n + b * n + c)
    have nn_le_nn: n * n ≤ n * n by .
    have nn_le_ann: n * n ≤ a * n * n
      by apply uint_mult_mono_le2[1, n*n, a, n*n] to a_pos, nn_le_nn
    have ann_le_pluss: a * n * n ≤ a * n * n + b * n by uint_less_equal_add
    have nn_le_first2: n * n ≤ a * n * n + b * n
      by apply uint_less_equal_trans to nn_le_ann, ann_le_pluss
    have last_le: a * n * n + b * n ≤ a * n * n + b * n + c by uint_less_equal_add
    apply uint_less_equal_trans to nn_le_first2, last_le
  }
  upper, lower
end

// Polynomial closure, degree 3: a degree-3 polynomial with positive leading
// coefficient is asymptotically equivalent to its leading monomial.
// `a*n*n*n + b*n*n + c*n + d ≈ n*n*n` when `1 ≤ a`. Upper bound at `n0 = 1`,
// `c0 = a + b + c + d`: each lower-order term is dominated by a constant
// multiple of `n*n*n` since `n*n ≤ n*n*n`, `n ≤ n*n*n`, and `1 ≤ n*n*n` for
// `n ≥ 1`. Lower bound at `n0 = 0`, `c0 = 1`: `1 ≤ a` gives
// `n*n*n ≤ a*(n*n*n) ≤ a*n*n*n + b*n*n + c*n + d` pointwise.
theorem bigo_cubic_closure: all a:UInt, b:UInt, c:UInt, d:UInt.
  if 1 ≤ a then (fun n:UInt { a * n * n * n + b * n * n + c * n + d })
              ≈ (fun n:UInt { n * n * n })
proof
  arbitrary a:UInt, b:UInt, c:UInt, d:UInt
  assume a_pos: 1 ≤ a
  expand operator≈
  have upper: (fun n:UInt { a * n * n * n + b * n * n + c * n + d })
            ≲ (fun n:UInt { n * n * n }) by {
    expand operator≲
    choose 1, a + b + c + d
    arbitrary n:UInt
    assume n_ge_1: 1 ≤ n
    show a * n * n * n + b * n * n + c * n + d ≤ (a + b + c + d) * (n * n * n)
    have n_le_n: n ≤ n by .
    have n_le_nn: n ≤ n * n
      by apply uint_mult_mono_le2[1, n, n, n] to n_ge_1, n_le_n
    have one_le_nn: 1 ≤ n * n
      by apply uint_less_equal_trans to n_ge_1, n_le_nn
    have nn_le_nn: n * n ≤ n * n by .
    have nn_le_nnn: n * n ≤ n * n * n
      by apply uint_mult_mono_le2[1, n*n, n, n*n] to n_ge_1, nn_le_nn
    have n_le_nnn: n ≤ n * n * n
      by apply uint_less_equal_trans to n_le_nn, nn_le_nnn
    have one_le_nnn: 1 ≤ n * n * n
      by apply uint_less_equal_trans to n_ge_1, n_le_nnn
    have annn_le: a * n * n * n ≤ a * (n * n * n) by .
    have bnn_le_bnn: b * n * n ≤ b * (n * n) by .
    have bnn_le_bnnn_lifted: b * (n * n) ≤ b * (n * n * n)
      by apply uint_mult_mono_le[b, n*n, n*n*n] to nn_le_nnn
    have bnn_le_bnnn: b * n * n ≤ b * (n * n * n)
      by apply uint_less_equal_trans to bnn_le_bnn, bnn_le_bnnn_lifted
    have cn_le_cnnn: c * n ≤ c * (n * n * n)
      by apply uint_mult_mono_le[c, n, n*n*n] to n_le_nnn
    have d_le_dnnn: d ≤ d * (n * n * n)
      by apply uint_mult_mono_le[d, 1, n*n*n] to one_le_nnn
    have sum1: a * n * n * n + b * n * n ≤ a * (n * n * n) + b * (n * n * n)
      by apply uint_add_mono_less_equal to annn_le, bnn_le_bnnn
    have sum2: a * n * n * n + b * n * n + c * n
             ≤ a * (n * n * n) + b * (n * n * n) + c * (n * n * n)
      by apply uint_add_mono_less_equal to sum1, cn_le_cnnn
    have sum3: a * n * n * n + b * n * n + c * n + d
             ≤ a * (n * n * n) + b * (n * n * n) + c * (n * n * n) + d * (n * n * n)
      by apply uint_add_mono_less_equal to sum2, d_le_dnnn
    have expand_eq: (a + b + c + d) * (n * n * n)
                  = a * (n * n * n) + b * (n * n * n) + c * (n * n * n) + d * (n * n * n) by {
      have step1: (a + b + c + d) * (n * n * n)
                = (a + b + c) * (n * n * n) + d * (n * n * n)
        by uint_dist_mult_add_right[a + b + c, d, n * n * n]
      have step2: (a + b + c) * (n * n * n)
                = (a + b) * (n * n * n) + c * (n * n * n)
        by uint_dist_mult_add_right[a + b, c, n * n * n]
      have step3: (a + b) * (n * n * n)
                = a * (n * n * n) + b * (n * n * n)
        by uint_dist_mult_add_right[a, b, n * n * n]
      replace step1 | step2 | step3.
    }
    replace expand_eq
    sum3
  }
  have lower: (fun n:UInt { n * n * n })
            ≲ (fun n:UInt { a * n * n * n + b * n * n + c * n + d }) by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show n * n * n ≤ 1 * (a * n * n * n + b * n * n + c * n + d)
    have nnn_le_nnn: n * n * n ≤ n * n * n by .
    have nnn_le_annn: n * n * n ≤ a * n * n * n
      by apply uint_mult_mono_le2[1, n*n*n, a, n*n*n] to a_pos, nnn_le_nnn
    have annn_le_p1: a * n * n * n ≤ a * n * n * n + b * n * n
      by uint_less_equal_add
    have nnn_le_p1: n * n * n ≤ a * n * n * n + b * n * n
      by apply uint_less_equal_trans to nnn_le_annn, annn_le_p1
    have p1_le_p2: a * n * n * n + b * n * n ≤ a * n * n * n + b * n * n + c * n
      by uint_less_equal_add
    have nnn_le_p2: n * n * n ≤ a * n * n * n + b * n * n + c * n
      by apply uint_less_equal_trans to nnn_le_p1, p1_le_p2
    have p2_le_p3: a * n * n * n + b * n * n + c * n
                 ≤ a * n * n * n + b * n * n + c * n + d
      by uint_less_equal_add
    apply uint_less_equal_trans to nnn_le_p2, p2_le_p3
  }
  upper, lower
end

// Generic polynomial evaluation in Horner form. Given a list of
// coefficients `[a_0, a_1, ..., a_k]` (low-degree first), evaluates the
// polynomial `a_0 + a_1*n + a_2*n^2 + ... + a_k*n^k`.
recursive poly_eval(List<UInt>, UInt) -> UInt {
  poly_eval(empty, n) = 0
  poly_eval(node(a, rest), n) = a + n * poly_eval(rest, n)
}

// Sum of the elements of a `List`. Used to bound polynomials
// from above by a constant times the leading monomial.
recursive sum_coeffs(List<UInt>) -> UInt {
  sum_coeffs(empty) = 0
  sum_coeffs(node(a, rest)) = a + sum_coeffs(rest)
}

// Pointwise upper bound for `poly_eval` on a polynomial whose
// coefficients have the form `pre ++ [a]` (leading coefficient `a`,
// degree `length(pre)`): for `n ≥ 1`,
// `poly_eval(pre ++ [a], n) ≤ (a + sum_coeffs(pre)) * n^(length(pre))`.
// Proof by induction on `pre`; the constant is built up term by term.
lemma poly_eval_upper_bound:
  all pre:List<UInt>. all a:UInt, n:UInt.
  if 1 ≤ n
  then poly_eval(pre ++ [a], n) ≤ (a + sum_coeffs(pre)) * n^(length(pre))
proof
  induction List<UInt>
  case empty {
    arbitrary a:UInt, n:UInt
    assume one_le_n: 1 ≤ n
    expand operator++ | 2 * poly_eval | sum_coeffs | length.
  }
  case node(b, rest) suppose IH:
      (all a:UInt, n:UInt. if 1 ≤ n
       then poly_eval(rest ++ [a], n) ≤ (a + sum_coeffs(rest)) * n^(length(rest))) {
    arbitrary a:UInt, n:UInt
    assume one_le_n: 1 ≤ n
    have ih: poly_eval(rest ++ [a], n) ≤ (a + sum_coeffs(rest)) * n^(length(rest))
      by apply IH[a, n] to one_le_n
    expand operator++ | poly_eval | sum_coeffs | length
    show b + n * poly_eval(rest ++ [a], n)
       ≤ (a + (b + sum_coeffs(rest))) * n^(1 + length(rest))
    have pow_next: n^(1 + length(rest)) = n * n^(length(rest))
      by uint_pow_add_r[n, 1, length(rest)]
    have one_le_pow_next: 1 ≤ n^(1 + length(rest))
      by apply uint_pow_le_mono_l[1 + length(rest), 1, n] to one_le_n
    have step_mult: n * poly_eval(rest ++ [a], n)
                  ≤ n * ((a + sum_coeffs(rest)) * n^(length(rest)))
      by apply uint_mult_mono_le[n, poly_eval(rest ++ [a], n),
                                 (a + sum_coeffs(rest)) * n^(length(rest))]
         to ih
    have rearrange: n * ((a + sum_coeffs(rest)) * n^(length(rest)))
                  = (a + sum_coeffs(rest)) * n^(1 + length(rest)) by {
      equations
        n * ((a + sum_coeffs(rest)) * n^(length(rest)))
            = (a + sum_coeffs(rest)) * (n * n^(length(rest)))
              by replace uint_mult_commute[n, a + sum_coeffs(rest)].
        ... = # (a + sum_coeffs(rest)) * n^(1 + length(rest)) #
              by replace pow_next.
    }
    have step_mult2: n * poly_eval(rest ++ [a], n)
                   ≤ (a + sum_coeffs(rest)) * n^(1 + length(rest))
      by replace rearrange in step_mult
    have b_le_b_pow: b ≤ b * n^(1 + length(rest))
      by apply uint_mult_mono_le[b, 1, n^(1 + length(rest))] to one_le_pow_next
    have sum_bound: b + n * poly_eval(rest ++ [a], n)
                  ≤ b * n^(1 + length(rest))
                  + (a + sum_coeffs(rest)) * n^(1 + length(rest))
      by apply uint_add_mono_less_equal to b_le_b_pow, step_mult2
    have factor: b * n^(1 + length(rest))
               + (a + sum_coeffs(rest)) * n^(1 + length(rest))
               = (a + (b + sum_coeffs(rest))) * n^(1 + length(rest)) by {
      have d1: b * n^(1 + length(rest))
             + (a + sum_coeffs(rest)) * n^(1 + length(rest))
             = (b + (a + sum_coeffs(rest))) * n^(1 + length(rest))
        by symmetric uint_dist_mult_add_right[b, a + sum_coeffs(rest),
                                              n^(1 + length(rest))]
      have rearr: b + a = a + b by uint_add_commute[b, a]
      replace d1 | rearr.
    }
    replace factor in sum_bound
  }
end

// Pointwise lower bound for `poly_eval` on a polynomial whose
// coefficients have the form `pre ++ [a]` with leading coefficient
// `a ≥ 1`: for every `n`, `n^(length(pre)) ≤ poly_eval(pre ++ [a], n)`.
// Proof by induction on `pre`; the base case uses `1 ≤ a`, the step
// multiplies the IH by `n` and absorbs the next coefficient via
// `uint_less_equal_add`.
lemma poly_eval_lower_bound:
  all pre:List<UInt>. all a:UInt.
  if 1 ≤ a then all n:UInt.
  n^(length(pre)) ≤ poly_eval(pre ++ [a], n)
proof
  induction List<UInt>
  case empty {
    arbitrary a:UInt
    assume one_le_a: 1 ≤ a
    arbitrary n:UInt
    expand operator++ | 2 * poly_eval | length
    one_le_a
  }
  case node(b, rest) suppose IH:
      (all a:UInt. if 1 ≤ a then all n:UInt.
       n^(length(rest)) ≤ poly_eval(rest ++ [a], n)) {
    arbitrary a:UInt
    assume one_le_a: 1 ≤ a
    arbitrary n:UInt
    have ih: n^(length(rest)) ≤ poly_eval(rest ++ [a], n)
      by apply IH[a] to one_le_a
    expand operator++ | poly_eval | length
    show n^(1 + length(rest)) ≤ b + n * poly_eval(rest ++ [a], n)
    have pow_next: n^(1 + length(rest)) = n * n^(length(rest))
      by uint_pow_add_r[n, 1, length(rest)]
    have step_mult: n * n^(length(rest)) ≤ n * poly_eval(rest ++ [a], n)
      by apply uint_mult_mono_le[n, n^(length(rest)),
                                 poly_eval(rest ++ [a], n)] to ih
    have absorb: n * poly_eval(rest ++ [a], n)
               ≤ b + n * poly_eval(rest ++ [a], n) by uint_less_equal_add_left
    have chain: n^(1 + length(rest))
              ≤ b + n * poly_eval(rest ++ [a], n) by {
      replace pow_next
      apply uint_less_equal_trans to step_mult, absorb
    }
    chain
  }
end

// Closure of polynomial expressions under `≈`. Any polynomial of the
// form `a_0 + a_1*n + a_2*n^2 + ... + a_k*n^k` with positive leading
// coefficient `a_k ≥ 1` is asymptotically equivalent to its leading
// monomial `n^k`. Stated via `pre ++ [a]` so that the leading
// coefficient is in evidence; `length(pre)` is the polynomial degree.
// Specializes the fixed-degree closures `bigo_linear_closure`,
// `bigo_quadratic_closure`, and `bigo_cubic_closure` to arbitrary
// degree, and supersedes the need to add one theorem per degree.
theorem bigo_poly_closure:
  all pre:List<UInt>, a:UInt.
  if 1 ≤ a
  then (fun n:UInt { poly_eval(pre ++ [a], n) })
     ≈ (fun n:UInt { n^(length(pre)) })
proof
  arbitrary pre:List<UInt>, a:UInt
  assume one_le_a: 1 ≤ a
  expand operator≈
  have upper: (fun n:UInt { poly_eval(pre ++ [a], n) })
            ≲ (fun n:UInt { n^(length(pre)) }) by {
    expand operator≲
    choose 1, a + sum_coeffs(pre)
    arbitrary n:UInt
    assume one_le_n: 1 ≤ n
    show poly_eval(pre ++ [a], n) ≤ (a + sum_coeffs(pre)) * n^(length(pre))
    apply poly_eval_upper_bound[pre][a, n] to one_le_n
  }
  have lower: (fun n:UInt { n^(length(pre)) })
            ≲ (fun n:UInt { poly_eval(pre ++ [a], n) }) by {
    expand operator≲
    choose 0, 1
    arbitrary n:UInt
    assume _
    show n^(length(pre)) ≤ 1 * poly_eval(pre ++ [a], n)
    have lb: all m:UInt. m^(length(pre)) ≤ poly_eval(pre ++ [a], m)
      by apply poly_eval_lower_bound[pre][a] to one_le_a
    lb[n]
  }
  upper, lower
end