Float.hj_of: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
Lines 267-269 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=267&end_line=269

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/logic.bend as L

# j <= 52 from the bit length 1 + j <= 53
def hj_of(+np: Nat, +j: Nat, +hf: {C.fits(53n, 1n+np) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {Nat.is_le(j, 52n) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, M.bit_length(1n+np), 1n+j, hbl, bl_le(53n, 1n+np, hf))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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_le
  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/math/random/float.bend&name=bl_le
  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/src/math/natural.bend&name=bit_length