Roots.done_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 143-146 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=143&end_line=146

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

# lo + 1 >= hi with lo < hi: the interval is [lo, lo + 1)
def done_ok(+n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +hlo: {M.root_le(n, k, lo) == True{} : Bool}, +hhi: {M.root_le(n, k, hi) == False{} : Bool}, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hm: {False{} == Nat.is_lt(1n+lo, hi) : Bool}) -> root_ok(n, k, lo):
  +e = N.le_antisym(hi, 1n+lo, N.not_lt_le(1n+lo, hi, Equal.sym(Bool, False{}, Nat.is_lt(1n+lo, hi), hm)), N.lt_succ_le_succ(lo, hi, hlt))
  (hlo, Equal.trans(Bool, M.root_le(n, k, 1n+lo), M.root_le(n, k, hi), False{}, Equal.cong(Nat, Bool, z => M.root_le(n, k, z), 1n+lo, hi, Equal.sym(Nat, hi, 1n+lo, e)), hhi))

Uses (12):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_antisym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend&name=root_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=root_le