def f53h

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:176

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

176def f53h(+q: Nat) -> {C.fits(53n, q) == Nat.is_eq(C.half(C.high(52n, q)), 0n) : Bool}:
177  fits_hc(52n, 1n, q)