Fround.bl_c: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
Lines 123-133 of bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&start_line=123&end_line=133

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/proofs/lib/nat.bend as N
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/natcmp.bend as NC
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/bits.bend as BT

def bl_c(+k: Nat, +n: Nat, +h1: {C.fits(k, n) == False{} : Bool}, +h2: {C.fits(1n+k, n) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(M.bit_length(n), 1n+k) == c : Cmp}) -> {M.bit_length(n) == 1n+k : Nat}:
  match c:
    case EQ{}:
      NC.eq_of_cmp(M.bit_length(n), 1n+k, hc)
    case LT{}:
      +hl = N.lt_succ_le(M.bit_length(n), k, NC.lt_of_cmp(M.bit_length(n), 1n+k, hc))
      +hn = N.lt_le_trans(n, C.pow2(M.bit_length(n)), C.pow2(k), BT.bit_length_lt(n), N.pow2_mono(M.bit_length(n), k, hl))
      NC.absurd_tf({M.bit_length(n) == 1n+k : Nat}, Equal.trans(Bool, False{}, C.fits(k, n), True{}, Equal.sym(Bool, C.fits(k, n), False{}, h1), WW.fits_of_lt(k, n, hn)))
    case GT{}:
      +hg = N.pow2_mono(2n+k, M.bit_length(n), N.lt_succ_le_succ(1n+k, M.bit_length(n), NC.lt_of_gt(M.bit_length(n), 1n+k, hc)))
      bl_gt(k, n, h1, h2, hg)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le
  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=pow2_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend&name=bit_length_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bl_gt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=absurd_tf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=eq_of_cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=lt_of_cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=lt_of_gt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=fits_of_lt
  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/src/math/natural.bend&name=bit_length