def cnt2

bendtorch@1.3.0.0 · PROOF.bend:1038

import Base
import bendtorch@1.3.0.0/spec.bend as Spec
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

1038# 2^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k)
1039def cnt2(+p: Nat, +k: Nat) -> {Nat.mul(Spec.pw(1n+p), k) == Nat.mul(Spec.pw(p), Nat.add(k, k)) : Nat}:
1040  +a = Spec.pw(p)
1041  Equal.trans(Nat, Nat.mul(Nat.add(a, a), k), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(a, Nat.add(k, k)),
1042    Equal.sym(Nat, Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(Nat.add(a, a), k), NL.mul_dist(a, a, k)),
1043    Equal.sym(Nat, Nat.mul(a, Nat.add(k, k)), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), NL.mul_dist_l(a, k, k)))