def fit_td

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:176

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

176# a bit t <= 1 below 2 y leaves the width of y
177def fit_td(+a: Nat, +t: Nat, +y: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.fits(1n+a, Nat.add(t, Nat.double(y))) == C.fits(a, y) : Bool}:
178  Equal.cong(Nat, Bool, z => C.fits(a, z), C.half(Nat.add(t, Nat.double(y))), y, Equal.trans(Nat, C.half(Nat.add(t, Nat.double(y))), Nat.add(C.half(t), y), y, WW.half_dbl(t, y), Equal.cong(Nat, Nat, z => Nat.add(z, y), C.half(t), 0n, FR.half_small(t, ht))))