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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as RT

# with no fuel left k == n, and p b <= n is impossible: n == k < p <= p b
def ilog_absurd(+n: Nat, +bq: Nat, +k: Nat, +p: Nat, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hu: {True{} == Nat.is_le(Nat.mul(p, 2n+bq), n) : Bool}, +hf: {k == n : Nat}) -> Empty:
  +b = {2n+bq : Nat}
  +kp = Equal.trans(Bool, Nat.is_lt(k, p), Nat.is_lt(k, Nat.pow(b, k)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(k, z), p, Nat.pow(b, k), hp), pow_gt(bq, k))
  +kb = N.lt_le_trans(k, p, Nat.mul(p, b), kp, RT.le_mul_pos(p, b, {==}))
  +kn = N.lt_le_trans(k, Nat.mul(p, b), n, kb, Equal.sym(Bool, True{}, Nat.is_le(Nat.mul(p, b), n), hu))
  N.lt_ne(k, n, kn, hf)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  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.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=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_ne
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/logs.bend&name=pow_gt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&name=le_mul_pos