def low_sh

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:32

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

32def low_sh(+d: Nat, +k: Nat, +m: Nat, +hd: {Nat.is_le(d, k) == True{} : Bool}) -> {C.low(d, C.shift(k, m)) == 0n : Nat}:
33  +es = NC.sh_split(k, d, m, hd)
34  Equal.trans(Nat, C.low(d, C.shift(k, m)), C.low(d, Nat.add(0n, C.shift(d, C.shift(Nat.sub(k, d), m)))), 0n, Equal.cong(Nat, Nat, z => C.low(d, z), C.shift(k, m), C.shift(d, C.shift(Nat.sub(k, d), m)), es), WW.low_u(d, 0n, C.shift(Nat.sub(k, d), m), FR.fz(d)))