def ok_lt
bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:235
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as Roots
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
235def 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}:
236 (a, b) = p
237 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))