def pow_gt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/logs.bend:25

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

25# k < b^k for b >= 2
26def pow_gt(+bq: Nat, +k: Nat) -> {Nat.is_lt(k, Nat.pow(2n+bq, k)) == True{} : Bool}:
27  match k:
28    case 0n:
29      {==}
30    case 1n+ +kp:
31      +p = Nat.pow(2n+bq, kp)
32      +q = Nat.add(p, Nat.mul(bq, p))
33      +hp = N.lt_succ_le_succ(kp, p, pow_gt(bq, kp))
34      +hq = N.lt_le_trans(0n, p, q, RT.pow_pos(1n+bq, kp), N.le_add_right(p, Nat.mul(bq, p)))
35      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))