def low_shift0
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:27
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as Montnat
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
27def low_shift0(+kk: Nat, +z: Nat) -> {C.low(kk, C.shift(kk, z)) == 0n : Nat}:
28 Equal.trans(Nat, C.low(kk, C.shift(kk, z)), C.low(kk, 0n), 0n, WW.low_add_shift(kk, 0n, z), low_zero(kk))