def hfit
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rint.bend:118
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend as F64rint
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/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
118def hfit(+j: Nat, +V: Nat, +hv: {C.fits(64n, V) == True{} : Bool}) -> {C.fits(63n, C.high(1n+j, V)) == True{} : Bool}:
119 +f = SH.fits_mono(64n, Nat.add(1n+j, 63n), V, le64(j), hv)
120 Equal.trans(Bool, C.fits(63n, C.high(1n+j, V)), C.fits(Nat.add(1n+j, 63n), V), True{}, Equal.sym(Bool, C.fits(Nat.add(1n+j, 63n), V), C.fits(63n, C.high(1n+j, V)), FR.fits_hc(1n+j, 63n, V)), f)