def shift_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:163

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

163def shift_zero(+k: Nat) -> {C.shift(k, 0n) == 0n : Nat}:
164  match k:
165    case 0n:
166      {==}
167    case 1n+ +p:
168      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, 0n), 0n, shift_zero(p))