Bitsrel.sh_idx: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend as Bitsrel
Lines 97-99 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend&start_line=97&end_line=99

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

def sh_idx(+j: Nat, +d: Nat, +r: Nat) -> {C.shift(Nat.add(1n+j, d), r) == C.shift(Nat.add(j, 1n+d), r) : Nat}:
  %Equal.sym(Nat, Nat.add(j, 1n+d), 1n+Nat.add(j, d), NA.add_succ(j, d)) : {C.shift(Nat.add(1n+j, d), r) == C.shift(_, r) : 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/lib/lemmas/proofs/nat_algebra.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift