def go_sb
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pmul.bend:22
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as Pmul
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend as BR
22def go_sb(i: Nat, +k: Nat) -> {CV.bits_go(i, k) == BR.sb(i, 0n, k) : List<&2, Nat>}:
23 match i:
24 case 0n:
25 {==}
26 case 1n+ +j:
27 Equal.cong(List<&2, Nat>, List<&2, Nat>, l => CV.bit(j, k) <> l, CV.bits_go(j, k), BR.sb(j, 0n, k), go_sb(j, k))