Roots.ok_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as Roots
Lines 235-237 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&start_line=235&end_line=237

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/src/math/natural.bend as M

def ok_lt(+n: Nat, +k: Nat, +r: Nat, p: root_ok(n, k, r)) -> {Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool}:
  (a, b) = p
  N.not_le_lt(Nat.pow(1n+r, k), n, Equal.trans(Bool, Nat.is_le(Nat.pow(1n+r, k), n), M.root_le(n, k, 1n+r), False{}, Equal.sym(Bool, M.root_le(n, k, 1n+r), Nat.is_le(Nat.pow(1n+r, k), n), root_le_ok(n, k, 1n+r)), b))

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=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.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=not_le_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&name=root_le_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend&name=root_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend&name=root_le