def ef11

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

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

775def ef11(+EF: Nat, +c: Nat, +hov: {Nat.is_lt(Nat.add(EF, c), 2047n) == True{} : Bool}) -> {C.fits(11n, EF) == True{} : Bool}:
776  WW.fits_of_lt(11n, EF, N.le_lt_trans(EF, Nat.add(EF, c), 2048n, N.le_add_right(EF, c), N.lt_trans(Nat.add(EF, c), 2047n, 2048n, hov, {==})))