Logs.pow_gt: 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 25-35 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=25&end_line=35

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

# k < b^k for b >= 2
def pow_gt(+bq: Nat, +k: Nat) -> {Nat.is_lt(k, Nat.pow(2n+bq, k)) == True{} : Bool}:
  match k:
    case 0n:
      {==}
    case 1n+ +kp:
      +p = Nat.pow(2n+bq, kp)
      +q = Nat.add(p, Nat.mul(bq, p))
      +hp = N.lt_succ_le_succ(kp, p, pow_gt(bq, kp))
      +hq = N.lt_le_trans(0n, p, q, RT.pow_pos(1n+bq, kp), N.le_add_right(p, Nat.mul(bq, p)))
      N.lt_le_trans(1n+kp, Nat.add(1n+kp, q), Nat.add(p, q), lt_add_pos(1n+kp, q, hq), le_add_r(1n+kp, p, q, hp))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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=le_add_right
  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_succ_le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/logs.bend&name=le_add_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/logs.bend&name=lt_add_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&name=pow_pos