def ok_le
bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:231
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/src/math/natural.bend as M
231def ok_le(+n: Nat, +k: Nat, +r: Nat, p: root_ok(n, k, r)) -> {Nat.is_le(Nat.pow(r, k), n) == True{} : Bool}:
232 (a, b) = p
233 Equal.trans(Bool, Nat.is_le(Nat.pow(r, k), n), M.root_le(n, k, r), True{}, Equal.sym(Bool, M.root_le(n, k, r), Nat.is_le(Nat.pow(r, k), n), root_le_ok(n, k, r)), a)