def top_q

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

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

179def top_q(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +hf: {C.fits(53n, q) == False{} : Bool}) -> {q == C.shift(52n, Nat.double(one)) : Nat}:
180  +hlt = Equal.trans(Bool, Nat.is_lt(q, C.shift(53n, one)), C.fits(53n, q), False{}, lt_fit(53n, one, h1, q), hf)
181  +hge = N.not_lt_le(q, C.shift(53n, one), hlt)
182  Equal.trans(Nat, q, C.shift(53n, one), C.shift(52n, Nat.double(one)), N.le_antisym(q, C.shift(53n, one), hq, hge), Equal.sym(Nat, C.shift(52n, Nat.double(one)), C.shift(53n, one), WW.shift_dbl(52n, one)))