def shift_one

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

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

177def shift_one(+k: Nat) -> {C.shift(k, 1n) == C.pow2(k) : Nat}:
178  match k:
179    case 0n:
180      {==}
181    case 1n+ +p:
182      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, 1n), C.pow2(p), shift_one(p))