def root_below_c

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

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

528# x^k <= n < (1 + r)^k gives x <= r
529def root_below_c(+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}, +c: Bool, +hc: {Nat.is_lt(r, x) == c : Bool}) -> {Nat.is_le(x, r) == True{} : Bool}:
530  match c:
531    case True{}:
532      +h1 = N.le_trans(Nat.pow(1n+r, k), Nat.pow(x, k), n, pow_mono(1n+r, x, k, N.lt_succ_le_succ(r, x, hc)), hx)
533      Empty.absurd({Nat.is_le(x, r) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(n, Nat.pow(1n+r, k)), False{}, Equal.sym(Bool, Nat.is_lt(n, Nat.pow(1n+r, k)), True{}, hr), N.le_not_lt(n, Nat.pow(1n+r, k), h1))))
534    case False{}:
535      N.not_lt_le(r, x, hc)