def root_above_c

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

540# x^k > n >= r^k gives r < x
541def root_above_c(+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}, +c: Bool, +hc: {Nat.is_le(x, r) == c : Bool}) -> {Nat.is_lt(r, x) == True{} : Bool}:
542  match c:
543    case True{}:
544      Empty.absurd({Nat.is_lt(r, x) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_le(Nat.pow(x, k), n), False{}, Equal.sym(Bool, Nat.is_le(Nat.pow(x, k), n), True{}, N.le_trans(Nat.pow(x, k), Nat.pow(r, k), n, pow_mono(x, r, k, hc), hr)), hx)))
545    case False{}:
546      N.not_le_lt(x, r, hc)