F64bl.lower: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as F64bl
Lines 79-87 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend&start_line=79&end_line=87

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/natural/bits.bend as BT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

def lower(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(C.pow2(Nat.sub(M.bit_length(n), 1n)), n) == True{} : Bool}:
  match n:
    case 0n:
      Empty.absurd({Nat.is_le(C.pow2(Nat.sub(M.bit_length(0n), 1n)), 0n) == True{} : Bool}, LW.true_ne_false(hz))
    case 1n+ +np:
      +B = M.bit_length(1n+np)
      +eb = N.sub_add(B, 1n, bl_pos(1n+np, hz, B, {==}))
      +h1 = L.subst(Nat, z => {Nat.is_le(C.pow2(z), Nat.double(1n+np)) == True{} : Bool}, B, 1n+Nat.sub(B, 1n), Equal.sym(Nat, 1n+Nat.sub(B, 1n), B, eb), BT.bit_length_le(np))
      dle(C.pow2(Nat.sub(B, 1n)), 1n+np, h1)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.double
  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.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=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend&name=bit_length_le
  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=dle
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=true_ne_false
  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/src/math/natural.bend&name=bit_length