Bounds.pos_shift: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as Bounds
Lines 28-36 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&start_line=28&end_line=36

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/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

# 2^(16 n) y
def pos_shift(n: Nat, +y: Nat) -> {LV.pos(n, y) == C.shift(Nat.mul(n, 16n), y) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +k:
      %Equal.sym(Nat, LV.pos(k, y), C.shift(Nat.mul(k, 16n), y), pos_shift(k, y)) : {C.shift(16n, _) == C.shift(Nat.add(16n, Nat.mul(k, 16n)), y) : Nat}
      %Equal.sym(Nat, C.shift(Nat.add(16n, Nat.mul(k, 16n)), y), C.shift(16n, C.shift(Nat.mul(k, 16n), y)), Equal.sym(Nat, C.shift(16n, C.shift(Nat.mul(k, 16n), y)), C.shift(Nat.add(16n, Nat.mul(k, 16n)), y), SR.shift_shift(16n, Nat.mul(k, 16n), y))) : {C.shift(16n, C.shift(Nat.mul(k, 16n), y)) == _ : Nat}
      {==}

Uses (7):
  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=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=shift_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift