def round_shift_to

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

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

154# round_shift with the new exponent y == x + k given (a literal at the use), so
155# the result needs no conversion of Nat.add(x, k) inside SF.round
156def round_shift_to(+s: Bool, +k: Nat, +m: Nat, +x: Nat, +y: Nat, +hy: {Nat.add(x, k) == y : Nat}) -> {SF.round(s, C.shift(k, m), x) == SF.round(s, m, y) : F.F64}:
157  Equal.trans(F.F64, SF.round(s, C.shift(k, m), x), SF.round(s, m, Nat.add(x, k)), SF.round(s, m, y), round_shift(s, k, m, x), Equal.cong(Nat, F.F64, z => SF.round(s, m, z), Nat.add(x, k), y, hy))