def root_above

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

import Base

548def root_above(+r: Nat, +x: Nat, +k: Nat, +n: Nat, +hx: {Nat.is_le(Nat.pow(x, k), n) == False{} : Bool}, +hr: {Nat.is_le(Nat.pow(r, k), n) == True{} : Bool}) -> {Nat.is_lt(r, x) == True{} : Bool}:
549  root_above_c(r, x, k, n, hx, hr, Nat.is_le(x, r), {==})