~/jendhub

def done_ok

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:143

import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as Roots
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

143# lo + 1 >= hi with lo < hi: the interval is [lo, lo + 1)
144def 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):
145  +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))
146  (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)

Used by (1)