~/jendhub

def pow2_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/shrn.bend:124

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrn
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

124def pow2_eq(+k: Nat) -> {C.pow2(k) == 1n+Nat.sub(C.pow2(k), 1n) : Nat}:
125  Equal.sym(Nat, 1n+Nat.sub(C.pow2(k), 1n), C.pow2(k), N.sub_add(C.pow2(k), 1n, N.pow2_pos(k)))

Uses (6)

Used by (1)