def f53h

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:497

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

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