Roots.root_le_ok: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as Roots
Lines 54-64 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&start_line=54&end_line=64

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC

# root_le(n, k, r) is r^k <= n
def root_le_ok(+n: Nat, +k: Nat, +r: Nat) -> {M.root_le(n, k, r) == Nat.is_le(Nat.pow(r, k), n) : Bool}:
  match k r:
    case 0n r0:
      {==}
    case 1n+ +kp 0n:
      Equal.sym(Bool, Nat.is_le(0n, n), True{}, N.zero_le(n))
    case 1n+ +kp 1n+ +rp:
      +c = pow_le_case(kp, rp, 1n, n, Nat.is_le(1n, Nat.div(n, 1n+rp)), R.le_div(rp, 1n, n))
      %Equal.sym(Nat, Nat.pow(1n+rp, 1n+kp), Nat.mul(Nat.mul(1n, 1n+rp), Nat.pow(1n+rp, kp)), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.pow(1n+rp, kp)), 1n+rp, Nat.mul(1n, 1n+rp), Equal.sym(Nat, Nat.mul(1n, 1n+rp), 1n+rp, LC.one_mul(1n+rp)))) : {M.root_le(n, 1n+kp, 1n+rp) == Nat.is_le(_, n) : Bool}
      c

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=zero_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=le_div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=one_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&name=pow_le_case
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=root_le