def shift_pow2

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

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

198# shift(a, 2^b) == 2^(a + b)
199def shift_pow2(+a: Nat, +b: Nat) -> {C.shift(a, C.pow2(b)) == C.pow2(Nat.add(a, b)) : Nat}:
200  match a:
201    case 0n:
202      {==}
203    case 1n+ +p:
204      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, C.pow2(b)), C.pow2(Nat.add(p, b)), shift_pow2(p, b))