def root_below

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:537

import Base

537def root_below(+r: Nat, +x: Nat, +k: Nat, +n: Nat, +hx: {Nat.is_le(Nat.pow(x, k), n) == True{} : Bool}, +hr: {Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool}) -> {Nat.is_le(x, r) == True{} : Bool}:
538  root_below_c(r, x, k, n, hx, hr, Nat.is_lt(r, x), {==})