def j52
bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:243
import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC
243def j52(+np: Nat, +hf: {C.fits(53n, 1n+np) == True{} : Bool}) -> {Nat.is_le(J(np), 52n) == True{} : Bool}:
244 L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, M.bit_length(1n+np), 1n+J(np), WC.bl_succ(np), bl_le(53n, 1n+np, hf))