module UInt

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

lemma expt_dub_inc: all n:UInt, p:UInt. n ^ dub_inc(p) = sqr(n * (n^p))
proof
  arbitrary n:UInt, p:UInt
  expand operator^ | expt.
end

lemma expt_inc_dub: all n:UInt, p:UInt. n ^ inc_dub(p) = n * sqr(n^p)
proof
  arbitrary n:UInt, p:UInt
  expand operator^ | expt.
end

theorem toNat_expt: all p:UInt, n:UInt.
  toNat(n^p) = toNat(n) ^ toNat(p)
proof
  induction UInt
  case bzero {
    arbitrary n:UInt
    evaluate
  }
  case dub_inc(p') assume IH {
    arbitrary n:UInt
    replace expt_dub_inc
    expand toNat
    replace pow_add_r
    expand sqr
    replace toNat_mult | toNat_mult | toNat_mult | IH 
    define x = toNat(n)
    define p = toNat(p')
    replace symmetric pow_mul_r[p, x, ℕ2] | pow_mul_l
    replace mult_commute[x ^ p, x].
  }
  case inc_dub(x') assume IH {
    arbitrary n:UInt
    replace expt_inc_dub
    expand toNat
    replace nat_suc_one_add | pow_add_r | toNat_mult
    expand sqr
    replace toNat_mult | IH | symmetric pow_mul_r[toNat(x'), toNat(n), ℕ2]
    replace pow_mul_l.
  }
end

theorem fromNat_expt: all x:Nat, y:Nat.
  fromNat(x^y) = fromNat(x)^fromNat(y)
proof
  arbitrary x:Nat, y:Nat
  suffices toNat(fromNat(x^y)) = toNat(fromNat(x)^fromNat(y))
    by uint_toNat_injective
  replace toNat_expt | uint_toNat_fromNat.
end

theorem lit_expt_fromNat: all x:Nat, y:Nat.
  fromNat(lit(x)) ^ fromNat(lit(y)) = fromNat(lit(x) ^ lit(y))
proof
  arbitrary x:Nat, y:Nat
  symmetric fromNat_expt
end

auto lit_expt_fromNat

theorem uint_expt_zero: all n:UInt.
  n ^ 0 = 1
proof
  arbitrary n:UInt
  suffices toNat(n^0) = toNat(1)   by uint_toNat_injective
  equations
      toNat(n^0) = toNat(n)^toNat(0)  by toNat_expt
             ... = ℕ1 by replace uint_toNat_fromNat.
             ... = # toNat(1) #           by replace uint_toNat_fromNat.
end

auto uint_expt_zero
  
theorem uint_expt_suc: all n:UInt, m:Nat. n ^ fromNat(lit(suc(m))) = n * n ^ fromNat(lit(m))
proof
  arbitrary n:UInt, m:Nat
  suffices toNat(n ^ fromNat(lit(suc(m)))) = toNat(n * n ^ fromNat(lit(m))) by uint_toNat_injective
  replace toNat_mult | toNat_expt | uint_toNat_fromNat.
end
auto uint_expt_suc

theorem uint_expt_one: all n:UInt.
  n ^ 1 = n
proof
  arbitrary n:UInt
  suffices toNat(n^1) = toNat(n)   by uint_toNat_injective
  .
end

theorem uint_expt_two: all n:UInt.
  n ^ 2 = n * n
proof
  arbitrary n:UInt
  suffices toNat(n^2) = toNat(n * n) by uint_toNat_injective
  .
end

theorem uint_one_expt: all n:UInt.
  1 ^ n = 1
proof
  arbitrary n:UInt
  suffices toNat(1^n) = toNat(1) by uint_toNat_injective
  equations
      toNat(1^n) = toNat(1)^toNat(n)  by toNat_expt
             ... = ℕ1^toNat(n)        by { replace uint_toNat_fromNat. }
             ... = ℕ1                 by .
             ... = #toNat(1)#         by { replace uint_toNat_fromNat. }
end

theorem uint_pow_add_r : all m:UInt, n:UInt, o:UInt.
  m^(n + o) = m^n * m^o
proof
  arbitrary m:UInt, n:UInt, o:UInt
  suffices toNat(m^(n + o)) = toNat(m^n * m^o)  by uint_toNat_injective
  equations
      toNat(m^(n + o))
        = toNat(m) ^ toNat(n + o)           by toNat_expt
    ... = toNat(m) ^ (toNat(n) + toNat(o))  by replace toNat_add.
    ... = toNat(m) ^ toNat(n) * toNat(m) ^ toNat(o)  by replace pow_add_r.
    ... = #toNat(m^n) * toNat(m^o)#         by replace toNat_expt.
    ... = #toNat(m^n * m^o)#                by replace toNat_mult.
end

theorem uint_pow_mul_l : all m:UInt, n:UInt, o:UInt.
  (m * n)^o = m^o * n^o
proof
  arbitrary m:UInt, n:UInt, o:UInt
  suffices toNat((m * n)^o) = toNat(m^o * n^o)  by uint_toNat_injective
  equations
      toNat((m * n)^o)
        = toNat(m*n)^toNat(o)                   by replace toNat_expt.
    ... = (toNat(m)*toNat(n))^toNat(o)          by replace toNat_mult.
    ... = toNat(m)^toNat(o) * toNat(n)^toNat(o) by replace pow_mul_l.
    ... = #toNat(m^o) * toNat(n^o)#             by replace toNat_expt.
    ... = #toNat(m^o * n^o)#                    by replace toNat_mult.
end

theorem uint_pow_mul_r : all m : UInt, n : UInt, o : UInt.
  (m ^ n) ^ o = m ^ (n * o)
proof
  arbitrary m:UInt, n:UInt, o:UInt
  suffices toNat((m ^ n) ^ o) = toNat(m ^ (n * o))  by uint_toNat_injective
  equations
      toNat((m ^ n) ^ o)
        = (toNat(m) ^ toNat(n)) ^ toNat(o)   by replace toNat_expt | toNat_expt.
    ... = toNat(m) ^ (toNat(n) * toNat(o))   by pow_mul_r
    ... = #toNat(m ^ (n * o))#               by replace toNat_expt | toNat_mult.
end

theorem 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
proof
  arbitrary m:Nat, n:Nat, o:UInt
  symmetric uint_pow_mul_r[fromNat(lit(m)), fromNat(lit(n)), o]
end
auto lit_pow_mul_r

lemma pow_cnt_dubs_le_inc: all n:UInt. 2 ^ cnt_dubs(n) ≤ inc(n)
proof
  induction UInt
  case bzero {
    evaluate
  }
  case dub_inc(n') assume IH {
    expand cnt_dubs | inc
    replace inc_add_one | uint_pow_add_r | inc_dub_add_mult2 | uint_dist_mult_add
    show 2 * 2 ^ cnt_dubs(n') ≤ 3 + 2 * n'
    have IH': 2 ^ cnt_dubs(n') ≤ 1 + n' by replace inc_add_one in IH
    have A: 2 * 2 ^ cnt_dubs(n') ≤ 2 * (1 + n') by apply uint_mult_mono_le[2] to IH'
    have B: 2 * (1 + n') ≤ 3 + 2 * n' by {
      replace uint_dist_mult_add
      apply uint_add_mono_less_equal[2,2*n',3,2*n'] to .
    }
    apply uint_less_equal_trans to A, B
  }
  case inc_dub(n') assume IH {
    expand cnt_dubs | inc
    replace inc_add_one | uint_pow_add_r | dub_inc_mult2_add | uint_dist_mult_add
    show 2 * 2 ^ cnt_dubs(n') ≤ 2 + 2 * n'
    have IH': 2 ^ cnt_dubs(n') ≤ 1 + n' by replace inc_add_one in IH
    have A: 2 * 2 ^ cnt_dubs(n') ≤ 2 * (1 + n') by apply uint_mult_mono_le[2] to IH'
    have B: 2 * (1 + n') ≤ 2 + 2 * n' by replace uint_dist_mult_add.
    apply uint_less_equal_trans to A, B
  }
end

lemma cnt_le_cnt_dub: all x:UInt.
  cnt_dubs(x) ≤ cnt_dubs(dub(x)) 
proof
  induction UInt
  case bzero {
    expand dub.
  }
  case dub_inc(x') assume IH {
    expand dub | cnt_dubs | cnt_dubs
    replace inc_add_one | inc_add_one | uint_add_commute
    uint_less_equal_add
  }
  case inc_dub(x') assume IH {
    expand dub | cnt_dubs
    replace inc_add_one
    IH
  }
end

lemma cnt_dub_le_cnt: all x:UInt.
  cnt_dubs(dub(x)) ≤ 1 + cnt_dubs(x)
proof
  induction UInt
  case bzero {
    expand dub | cnt_dubs
    evaluate
  }
  case dub_inc(x') assume IH {
    expand dub | cnt_dubs | cnt_dubs
    replace inc_add_one | inc_add_one.
  }
  case inc_dub(x') assume IH {
    expand dub | cnt_dubs
    replace inc_add_one
    apply uint_add_both_sides_of_less_equal[1] to IH
  }
end

theorem log_pow: all n:UInt. log(2^n) = n
proof
  define P = fun n:UInt { log(2^n) = n }
  have base: P(0) by {
    expand P
    evaluate
  }
  have step: all m:UInt. if P(m) then P(1 + m) by {
    arbitrary m:UInt
    expand P
    assume IH: log(2^m) = m
    have pow_pos: 0 < 2^m by {
      have toNat0: toNat((0:UInt)) = zero by evaluate
      have toNat2: toNat((2:UInt)) = suc(suc(zero)) by evaluate
      apply less_toNat[0, 2^m] to {
        replace toNat_expt | toNat0 | toNat2
        have two_pos: zero < suc(suc(zero)) by evaluate
        apply pow_pos_nonneg[toNat(m), suc(suc(zero))] to two_pos
      }
    }
    obtain b where eq_pow: 2^m = 1 + b from apply uint_positive_add_one[2^m] to pow_pos
    have b_eq: pred(2^m) = b by {
      replace eq_pow
      replace symmetric inc_add_one[b]
      uint_pred_inc
    }
    have cnt_b: cnt_dubs(b) = m by {
      replace symmetric b_eq
      expand log in IH
    }
    have step_eq: 2^(1+m) = dub_inc(b) by {
      have h1: 2^(1+m) = 2 * 2^m by uint_pow_add_r[2, 1, m]
      have h2: 2 * 2^m = 2 * (1 + b) by replace eq_pow.
      have h3: 2 * (1 + b) = dub_inc(b) by symmetric dub_inc_mult2_add[b]
      transitive h1 (transitive h2 h3)
    }
    expand log
    replace step_eq
    expand pred | cnt_dubs
    replace cnt_b | inc_add_one.
  }
  expand P in apply uint_induction[P] to base, step
end
  
theorem uint_expt_log_less_equal: all n:UInt. if 0 < n then 2^log(n) ≤ n
proof
  arbitrary n:UInt
  assume pos
  obtain n' where n_n': n = 1 + n' from apply uint_positive_add_one[n] to pos
  replace n_n'
  expand log
  replace uint_pred_monus
  conclude 2 ^ cnt_dubs(n') ≤ 1 + n'
    by replace inc_add_one in pow_cnt_dubs_le_inc[n']
end


lemma inc_dub_less_dub : all n : UInt, m : UInt. if n < m then 1 + 2 * n < 2 * m
proof  
  arbitrary n : UInt, m : UInt
  assume prem
  have prem1 : 1 + n <= m by replace uint_less_is_less_equal[n][m] in prem
  have prem2 : 2 * (1 + n) <= 2 * m by apply uint_mult_mono_le[2] to prem1
  have prem3 : 1 + (1 + 2 * n) <= 2 * m by replace uint_dist_mult_add in prem2
  define g = 1 + 2 * n
  conclude g < 2 * m by replace symmetric uint_less_is_less_equal[g][2 * m] in prem3
end

lemma less_equal_pow_cnt_dubs: all n:UInt. 1 + n < 2 ^ (1 + cnt_dubs(n))
proof
  induction UInt
  case bzero {
    evaluate
  }
  case dub_inc(n') assume IH {
    expand cnt_dubs
    replace inc_add_one | uint_pow_add_r | dub_inc_mult2_add | uint_dist_mult_add
    show 3 + 2 * n' < 4 * 2 ^ cnt_dubs(n')
    have IH1: 1 + n' < 2 * 2 ^ cnt_dubs(n') by replace uint_pow_add_r in IH
    have IH2: 1 + 2*(1 + n') < 4 * 2 ^ cnt_dubs(n') 
      by apply inc_dub_less_dub[1+n', 2*2^cnt_dubs(n')] to ., IH1
    conclude 3 + 2*n' < 4 * 2 ^ cnt_dubs(n')
      by replace uint_dist_mult_add in IH2
  }
  case inc_dub(n') assume IH {
    expand cnt_dubs
    replace inc_add_one | uint_pow_add_r | inc_dub_add_mult2
    show 2 + 2 * n' < 4 * 2 ^ cnt_dubs(n')
    have IH1 : 2 * (1 + n') < 2 * 2 ^ (1 + cnt_dubs(n')) by
      apply uint_pos_mult_both_sides_of_less[2, 1+n', 2^(1+ cnt_dubs(n'))] to ., IH
    conclude  2 + 2 * n' < 4 * 2 ^ cnt_dubs(n') by
      replace uint_dist_mult_add[2, 1, n'] | uint_pow_add_r in IH1
  }
end

theorem less_pow_log: all n:UInt. if 0 < n then n < 2^(1 + log(n))
proof
  arbitrary n:UInt
  assume npos
  expand log
  replace uint_pred_monus
  obtain n' where n_n': n = 1 + n' from apply uint_positive_add_one[n] to npos
  replace n_n'
  less_equal_pow_cnt_dubs
end

/*
 The following rule is not literally true for UInt:
 log(3 * 3) = 3 ≠  1 + 1 = log(3) + log(3)

theorem log_product: all m:UInt, n:UInt. log(m * n) = log(m) + log(n)

 But it is true asymptotically...
  
*/

lemma cnt_dubs_mono: all y:UInt, x:UInt. if x ≤ y then cnt_dubs(x) ≤ cnt_dubs(y)
proof
  induction UInt
  case bzero {
    arbitrary x:UInt
    assume xle
    have x_z: x = bzero by apply uint_less_equal_bzero to xle
    replace x_z.
  }
  case dub_inc(y') assume IH {
    arbitrary x:UInt
    assume xle: x ≤ dub_inc(y')
    switch x {
      case bzero {
        expand cnt_dubs
        uint_bzero_le
      }
      case dub_inc(x') assume xeq {
        have step: x' ≤ y' by {
          have h: dub_inc(x') ≤ dub_inc(y') by replace xeq in xle
          have or_eq: dub_inc(x') < dub_inc(y') or dub_inc(x') = dub_inc(y') by expand operator≤ in h
          cases or_eq
          case lt {
            have hh: x' < y' by expand operator< in lt
            apply uint_less_implies_less_equal to hh
          }
          case eq {
            have hh: x' = y' by injective dub_inc eq
            replace hh.
          }
        }
        have ihres: cnt_dubs(x') ≤ cnt_dubs(y') by apply IH[x'] to step
        expand cnt_dubs
        replace inc_add_one
        apply uint_add_both_sides_of_less_equal[1] to ihres
      }
      case inc_dub(x') assume xeq {
        have step: x' ≤ y' by {
          have h: inc_dub(x') ≤ dub_inc(y') by replace xeq in xle
          have or_eq: inc_dub(x') < dub_inc(y') or inc_dub(x') = dub_inc(y') by expand operator≤ in h
          cases or_eq
          case lt {
            have hh: x' < y' or x' = y' by expand operator< in lt
            cases hh
            case llt { apply uint_less_implies_less_equal to llt }
            case leq { replace leq. }
          }
          case eq {
            // inc_dub = dub_inc impossible
            conclude false by evaluate in eq
          }
        }
        have ihres: cnt_dubs(x') ≤ cnt_dubs(y') by apply IH[x'] to step
        expand cnt_dubs
        replace inc_add_one
        apply uint_add_both_sides_of_less_equal[1] to ihres
      }
    }
  }
  case inc_dub(y') assume IH {
    arbitrary x:UInt
    assume xle: x ≤ inc_dub(y')
    switch x {
      case bzero {
        expand cnt_dubs
        uint_bzero_le
      }
      case dub_inc(x') assume xeq {
        have step: x' ≤ y' by {
          have h: dub_inc(x') ≤ inc_dub(y') by replace xeq in xle
          have or_eq: dub_inc(x') < inc_dub(y') or dub_inc(x') = inc_dub(y') by expand operator≤ in h
          cases or_eq
          case lt {
            have hh: x' < y' by expand operator< in lt
            apply uint_less_implies_less_equal to hh
          }
          case eq {
            conclude false by evaluate in eq
          }
        }
        have ihres: cnt_dubs(x') ≤ cnt_dubs(y') by apply IH[x'] to step
        expand cnt_dubs
        replace inc_add_one
        apply uint_add_both_sides_of_less_equal[1] to ihres
      }
      case inc_dub(x') assume xeq {
        have step: x' ≤ y' by {
          have h: inc_dub(x') ≤ inc_dub(y') by replace xeq in xle
          have or_eq: inc_dub(x') < inc_dub(y') or inc_dub(x') = inc_dub(y') by expand operator≤ in h
          cases or_eq
          case lt {
            have hh: x' < y' by expand operator< in lt
            apply uint_less_implies_less_equal to hh
          }
          case eq {
            have hh: x' = y' by injective inc_dub eq
            replace hh.
          }
        }
        have ihres: cnt_dubs(x') ≤ cnt_dubs(y') by apply IH[x'] to step
        expand cnt_dubs
        replace inc_add_one
        apply uint_add_both_sides_of_less_equal[1] to ihres
      }
    }
  }
end

lemma nat_pred_mono: all a:Nat. all b:Nat. if a ≤ b then pred(a) ≤ pred(b)
proof
  induction Nat
  case zero {
    arbitrary b:Nat
    assume _
    expand pred.
  }
  case suc(a') assume IH {
    arbitrary b:Nat
    assume hle
    switch b {
      case zero assume bz {
        conclude pred(suc(a')) ≤ pred(zero) by expand operator≤ in replace bz in hle
      }
      case suc(b') assume bs {
        expand pred
        expand operator≤ in replace bs in hle
      }
    }
  }
end

theorem uint_log_mono: all x:UInt, y:UInt. (if x ≤ y then log(x) ≤ log(y))
proof
  arbitrary x:UInt, y:UInt
  assume xle
  expand log
  have predle: pred(x) ≤ pred(y) by {
    apply less_equal_toNat[pred(x), pred(y)] to {
      replace toNat_pred
      have nle: toNat(x) ≤ toNat(y) by apply toNat_less_equal to xle
      apply nat_pred_mono[toNat(x), toNat(y)] to nle
    }
  }
  apply cnt_dubs_mono[pred(y), pred(x)] to predle
end

theorem uint_log_greater_one: all n:UInt. if 2 ≤ n then 1 ≤ log(n)
proof
  arbitrary n:UInt
  assume two_n
  have log2_1: log(2) = 1 by evaluate
  have one_log2: 1 ≤ log(2) by replace log2_1.
  have log2_logn: log(2) ≤ log(n) by apply uint_log_mono to two_n
  conclude 1 ≤ log(n)
    by apply uint_less_equal_trans to one_log2, log2_logn
end

lemma cnt_dub_less_n: all n:UInt. cnt_dubs(n) ≤ 1 + n
proof
  induction UInt
  case bzero {
    expand cnt_dubs
    uint_bzero_le
  }
  case dub_inc(n') assume IH {
    expand cnt_dubs
    replace dub_inc_mult2_add | inc_add_one | uint_dist_mult_add
    have less: 1 + n' ≤ 2 + 2 * n' by {
      have A: 1 + n' ≤ (1 + n') + (1 + n') by uint_less_equal_add
      have B: (1 + n') + (1 + n') ≤ 2 + 2*n'
        by replace uint_add_commute[n', 1] | symmetric uint_two_mult[n'].
      apply uint_less_equal_trans to A, B
    }
    apply uint_less_equal_trans to IH, less
  }
  case inc_dub(n') assume IH {
    expand cnt_dubs
    replace inc_dub_add_mult2 | inc_add_one
    have A: 1 + cnt_dubs(n') ≤ 2 + n'
      by apply uint_add_both_sides_of_less_equal[1] to IH
    have B: 2 + n' ≤ 2 + 2*n' by {
      have n_2n: n' ≤ 2*n' by {
        replace uint_two_mult
        uint_less_equal_add
      }
      apply uint_add_mono_less_equal[2, n', 2, 2*n'] to ., n_2n
    }
    apply uint_less_equal_trans to A, B
  }
end

theorem uint_logn_le_n: all n:UInt. log(n) ≤ n
proof
  arbitrary n:UInt
  expand log
  have X: cnt_dubs(pred(n)) ≤ 1 + pred(n) by cnt_dub_less_n[pred(n)]
  have Y: cnt_dubs(n ∸ 1) ≤ 1 + (n ∸ 1) by replace uint_pred_monus in X
  cases uint_zero_or_add_one[n]
  case nz {
    replace nz
    evaluate
  }
  case ns {
    obtain n' where n_n1: n = 1 + n' from ns
    replace n_n1 | uint_pred_monus
    replace n_n1 in Y
  }
end

// Without positivity premises this is false: e.g., m = 0, n = 4 gives
//   log(0) + log(4) = 0 + 2 = 2, log(0 * 4) = log(0) = 0, but 2 ≤ 0 is false.
postulate 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)

lemma uint_one_le_pow2: all k:UInt. 1 ≤ 2^k
proof
  arbitrary k:UInt
  have pow_pos: 0 < 2^k by {
    have toNat0: toNat((0:UInt)) = zero by evaluate
    have toNat2: toNat((2:UInt)) = suc(suc(zero)) by evaluate
    apply less_toNat[0, 2^k] to {
      replace toNat_expt | toNat0 | toNat2
      have two_pos: zero < suc(suc(zero)) by evaluate
      apply pow_pos_nonneg[toNat(k), suc(suc(zero))] to two_pos
    }
  }
  apply uint_pos_implies_one_le to pow_pos
end

lemma uint_pow2_mono: all a:UInt, b:UInt. if a ≤ b then 2^a ≤ 2^b
proof
  arbitrary a:UInt, b:UInt
  assume aleb: a ≤ b
  have step: a + (b ∸ a) = b by apply uint_monus_add_identity[b, a] to aleb
  have pow_eq: 2^b = 2^a * 2^(b ∸ a) by {
    replace symmetric step
    uint_pow_add_r[2, a, b ∸ a]
  }
  have one_le: 1 ≤ 2^(b ∸ a) by uint_one_le_pow2[b ∸ a]
  have mult_le: 2^a * 1 ≤ 2^a * 2^(b ∸ a) by apply uint_mult_mono_le[2^a] to one_le
  conclude 2^a ≤ 2^b by {
    replace pow_eq
    mult_le
  }
end

lemma uint_pow2_lt_implies_lt: all a:UInt, b:UInt. if 2^a < 2^b then a < b
proof
  arbitrary a:UInt, b:UInt
  assume powlt: 2^a < 2^b
  have tri: a < b or a = b or b < a by uint_trichotomy[a, b]
  cases tri
  case alb: a < b {
    alb
  }
  case aeb: a = b {
    have absurd: 2^a < 2^a by replace symmetric aeb in powlt
    conclude false by apply uint_less_irreflexive to absurd
  }
  case bla: b < a {
    have ble: b ≤ a by apply uint_less_implies_less_equal to bla
    have powle: 2^b ≤ 2^a by apply uint_pow2_mono[b, a] to ble
    have disj: 2^b < 2^a or 2^b = 2^a by expand operator≤ in powle
    have powlt2: 2^a < 2^a by {
      cases disj
      case lt: 2^b < 2^a {
        apply uint_less_trans to powlt, lt
      }
      case eq: 2^b = 2^a {
        conclude 2^a < 2^a by replace eq in powlt
      }
    }
    conclude false by apply uint_less_irreflexive to powlt2
  }
end

theorem uint_log_mult_le_log_add: all m:UInt, n:UInt. log(m * n) ≤ 1 + log(m) + log(n)
proof
  arbitrary m:UInt, n:UInt
  cases uint_zero_or_positive[m]
  case m_zero: m = 0 {
    replace m_zero
    have logz: log((0:UInt)) = 0 by evaluate
    replace logz
    uint_zero_le[1 + log(n)]
  }
  case m_pos: 0 < m {
    cases uint_zero_or_positive[n]
    case n_zero: n = 0 {
      replace n_zero
      have logz: log((0:UInt)) = 0 by evaluate
      replace logz
      uint_zero_le[1 + log(m) + 0]
    }
    case n_pos: 0 < n {
      have mn_pos: 0 < m * n
        by apply uint_pos_mult_both_sides_of_less[m, 0, n] to m_pos, n_pos
      have m_lt: m < 2^(1 + log(m)) by apply less_pow_log to m_pos
      have n_lt: n < 2^(1 + log(n)) by apply less_pow_log to n_pos
      have step1: m * n < 2^(1 + log(m)) * n by {
        have h: n * m < n * 2^(1 + log(m)) by apply uint_pos_mult_both_sides_of_less[n, m, 2^(1 + log(m))] to n_pos, m_lt
        replace uint_mult_commute[n, m] | uint_mult_commute[n, 2^(1 + log(m))] in h
      }
      have pow_pos_m: 0 < 2^(1 + log(m)) by {
        have one_le: 1 ≤ 2^(1 + log(m)) by uint_one_le_pow2[1 + log(m)]
        have one_pos: 0 < 1 by evaluate
        have or_eq: 1 < 2^(1 + log(m)) or 1 = 2^(1 + log(m)) by expand operator≤ in one_le
        cases or_eq
        case lt { apply uint_less_trans to one_pos, lt }
        case eq { replace symmetric eq one_pos }
      }
      have step2: 2^(1 + log(m)) * n < 2^(1 + log(m)) * 2^(1 + log(n))
        by apply uint_pos_mult_both_sides_of_less[2^(1 + log(m)), n, 2^(1 + log(n))] to pow_pos_m, n_lt
      have step3: m * n < 2^(1 + log(m)) * 2^(1 + log(n)) by apply uint_less_trans to step1, step2
      have pow_combine: 2^(1 + log(m)) * 2^(1 + log(n)) = 2^((1 + log(m)) + (1 + log(n))) by symmetric uint_pow_add_r[2, 1 + log(m), 1 + log(n)]
      have step4: m * n < 2^((1 + log(m)) + (1 + log(n))) by replace pow_combine in step3
      have step5: 2^log(m * n) ≤ m * n by apply uint_expt_log_less_equal to mn_pos
      have or_eq: 2^log(m * n) < m * n or 2^log(m * n) = m * n by expand operator≤ in step5
      have step6: 2^log(m * n) < 2^((1 + log(m)) + (1 + log(n))) by {
        cases or_eq
        case lt { apply uint_less_trans to lt, step4 }
        case eq { replace eq step4 }
      }
      have step7: log(m * n) < (1 + log(m)) + (1 + log(n)) by apply uint_pow2_lt_implies_lt to step6
      have step8: log(m * n) ≤ log(m) + 1 + log(n) by replace uint_less_is_less_equal in step7
      replace uint_add_commute[log(m), 1] in step8
    }
  }
end

theorem uint_log_pos: all n:UInt. (if 1 < n then 0 < log(n))
proof
  arbitrary n:UInt
  assume one_n: 1 < n
  have two_n: 2 ≤ n by replace uint_less_is_less_equal[1, n] in one_n
  have one_logn: 1 ≤ log(n) by apply uint_log_greater_one to two_n
  replace uint_less_is_less_equal[0, log(n)]
  one_logn
end