def shift_twice

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:25

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

25def shift_twice(+k: Nat, +x: Nat) -> {Nat.add(C.shift(k, x), C.shift(k, x)) == C.shift(1n+k, x) : Nat}:
26  Equal.sym(Nat, Nat.double(C.shift(k, x)), Nat.add(C.shift(k, x), C.shift(k, x)), NA.double_self(C.shift(k, x)))