def fit54

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

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

746# q < 2^53 + 1 fits 54 bits
747def fit54(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}) -> {C.fits(54n, q) == True{} : Bool}:
748  +h0 = L.subst(Nat, o => {Nat.is_lt(o, Nat.double(o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
749  +h2 = WW.shift_lt(53n, one, Nat.double(one), h0)
750  +h3 = L.subst(Nat, z => {Nat.is_lt(C.shift(53n, one), z) == True{} : Bool}, C.shift(53n, Nat.double(one)), C.shift(54n, one), WW.shift_dbl(53n, one), h2)
751  Equal.trans(Bool, C.fits(54n, q), Nat.is_lt(q, C.shift(54n, one)), True{}, Equal.sym(Bool, Nat.is_lt(q, C.shift(54n, one)), C.fits(54n, q), lt_fit(54n, one, h1, q)), N.le_lt_trans(q, C.shift(53n, one), C.shift(54n, one), hq, h3))