F64nrp.tbn: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend as F64nrp
Lines 54-60 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend&start_line=54&end_line=60

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL

def tbn(+k: Nat, +V: Nat, +K: Nat, +hz: {Nat.is_eq(V, 0n) == False{} : Bool}, +ek: {Nat.add(k, M.bit_length(V)) == 1n+K : Nat}) -> {C.fits(K, C.shift(k, V)) == False{} : Bool}:
  +epb = N.sub_add(M.bit_length(V), 1n, BL.bl_pos(V, hz, M.bit_length(V), {==}))
  +K2 = Nat.add(k, Nat.sub(M.bit_length(V), 1n))
  +e2 = N.succ_inj(K2, K, Equal.trans(Nat, 1n+K2, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K, Equal.sym(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K2, N.add_succ(k, Nat.sub(M.bit_length(V), 1n))), Equal.trans(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), Nat.add(k, M.bit_length(V)), 1n+K, Equal.cong(Nat, Nat, z => Nat.add(k, z), 1n+Nat.sub(M.bit_length(V), 1n), M.bit_length(V), epb), ek)))
  +hql = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, V)) == True{} : Bool}, C.shift(k, C.pow2(Nat.sub(M.bit_length(V), 1n))), C.pow2(K2), WW.shift_pow2(k, Nat.sub(M.bit_length(V), 1n)), WW.shift_mono(k, C.pow2(Nat.sub(M.bit_length(V), 1n)), V, BL.lower(V, hz)))
  +nf = Equal.trans(Bool, C.fits(K2, C.pow2(K2)), Nat.is_lt(C.pow2(K2), C.pow2(K2)), False{}, WW.fits_lt(K2, C.pow2(K2)), N.lt_irrefl(C.pow2(K2)))
  L.subst(Nat, z => {C.fits(z, C.shift(k, V)) == False{} : Bool}, K2, K, e2, FR.nfit(K2, C.pow2(K2), C.shift(k, V), hql, nf))

Uses (25):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_irrefl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=succ_inj
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend&name=bl_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend&name=lower
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=nfit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=fits_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=bit_length