def root_le

bend-collections@1.0.0.0 · src/math/natural.bend:189

import bend-collections@1.0.0.0/src/math/natural.bend as Natural

import Base

189def root_le(+n: Nat, +k: Nat, +r: Nat) -> Bool:
190  match k r:
191    case 0n _:
192      Nat.is_le(1n, n)
193    case 1n+kp 0n:
194      True{}
195    case 1n+ +kp 1n+ +rp:
196      pow_le_go(1n+kp, 1n+rp, 1n, n, Nat.is_le(1n, Nat.div(n, 1n+rp)))

Uses (5)

Used by (2)