def sh9
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adda.bend:90
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as F64adda
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/f64rtools.bend as RT
90def sh9(+k: Nat, +m: Nat, +h: {C.fits(k, m) == True{} : Bool}) -> {C.fits(Nat.add(9n, k), C.shift(9n, m)) == True{} : Bool}:
91 Equal.trans(Bool, C.fits(Nat.add(9n, k), C.shift(9n, m)), C.fits(k, m), True{}, RT.fits_sh(9n, k, m), h)