Logs.ilog_ok: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend as Logs
Lines 52-65 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend&start_line=52&end_line=65

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

# the loop: p == b^k <= n, up is p b <= n, fuel + k == n
def ilog_ok(fuel: Nat, +n: Nat, +bq: Nat, +k: Nat, +p: Nat, +up: Bool, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hpn: {Nat.is_le(p, n) == True{} : Bool}, +hup: {up == Nat.is_le(p, Nat.div(n, 2n+bq)) : Bool}, +hf: {Nat.add(fuel, k) == n : Nat}) -> {Nat.is_le(Nat.pow(2n+bq, M.ilog_go(fuel, n, 2n+bq, k, p, up)), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+M.ilog_go(fuel, n, 2n+bq, k, p, up))) == True{} : Bool}:
  match fuel up:
    case 0n False{}:
      ilog_stop(n, bq, k, p, hp, hpn, Equal.trans(Bool, False{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)))
    case 1n+f False{}:
      ilog_stop(n, bq, k, p, hp, hpn, Equal.trans(Bool, False{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)))
    case 0n True{}:
      Empty.absurd({Nat.is_le(Nat.pow(2n+bq, M.ilog_go(0n, n, 2n+bq, k, p, True{})), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+M.ilog_go(0n, n, 2n+bq, k, p, True{}))) == True{} : Bool}, ilog_absurd(n, bq, k, p, hp, Equal.trans(Bool, True{}, Nat.is_le(p, Nat.div(n, 2n+bq)), Nat.is_le(Nat.mul(p, 2n+bq), n), hup, R.le_div(1n+bq, p, n)), hf))
    case 1n+ +f True{}:
      +b = {2n+bq : Nat}
      +hu = Equal.trans(Bool, True{}, Nat.is_le(p, Nat.div(n, b)), Nat.is_le(Nat.mul(p, b), n), hup, R.le_div(1n+bq, p, n))
      +pb = Nat.mul(p, b)
      ilog_ok(f, n, bq, 1n+k, pb, Nat.is_le(pb, Nat.div(n, b)), Equal.trans(Nat, pb, Nat.mul(b, p), Nat.pow(b, 1n+k), A.mul_comm(p, b), Equal.cong(Nat, Nat, z => Nat.mul(b, z), p, Nat.pow(b, k), hp)), Equal.sym(Bool, True{}, Nat.is_le(pb, n), hu), {==}, Equal.trans(Nat, Nat.add(f, 1n+k), 1n+Nat.add(f, k), n, A.add_succ(f, k), hf))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=le_div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend&name=ilog_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend&name=ilog_stop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=ilog_go