def pow2_sq

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

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

417def pow2_sq(+k: Nat) -> {Nat.mul(C.pow2(k), C.pow2(k)) == C.pow2(Nat.add(k, k)) : Nat}:
418  Equal.trans(Nat, Nat.mul(C.pow2(k), C.pow2(k)), Nat.mul(C.pow2(k), C.shift(k, 1n)), C.pow2(Nat.add(k, k)), Equal.cong(Nat, Nat, t => Nat.mul(C.pow2(k), t), C.pow2(k), C.shift(k, 1n), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), shift_one(k))), Equal.trans(Nat, Nat.mul(C.pow2(k), C.shift(k, 1n)), C.shift(k, C.pow2(k)), C.pow2(Nat.add(k, k)), Equal.sym(Nat, C.shift(k, C.pow2(k)), Nat.mul(C.pow2(k), C.shift(k, 1n)), shift_mul(k, C.pow2(k))), shift_pow2(k, k)))