Lits.shk: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as Lits
Lines 13-17 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend&start_line=13&end_line=17

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/crypto/secp256k1/consts.bend as K

def shk(+k: Nat, +one: Nat, +v: Nat, +hv: {C.shift(k, one) == v : Nat}) -> {C.shift(1n+k, one) == Nat.add(v, v) : Nat}:
  %Equal.sym(Nat, C.shift(1n+k, one), Nat.add(C.shift(k, one), C.shift(k, one)), Equal.sym(Nat, Nat.add(C.shift(k, one), C.shift(k, one)), C.shift(1n+k, one), K.shift_twice(k, one))) : {_ == Nat.add(v, v) : Nat}
  %Equal.sym(Nat, C.shift(k, one), v, hv) : {Nat.add(_, C.shift(k, one)) == Nat.add(v, v) : Nat}
  %Equal.sym(Nat, C.shift(k, one), v, hv) : {Nat.add(v, _) == Nat.add(v, v) : Nat}
  {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=shift_twice
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift