def sb_last

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsrel.bend:49

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV

49# the last bit comes off the end
50def sb_last(j: Nat, +x: Nat) -> {sb(1n+j, 0n, x) == List.append(&2, Nat, sb(j, 1n, x), [CV.bit(0n, x)]) : List<&2, Nat>}:
51  match j:
52    case 0n:
53      {==}
54    case 1n+ +i:
55      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => CV.bit(1n+i, x) <> l, sb(1n+i, 0n, x), List.append(&2, Nat, sb(i, 1n, x), [CV.bit(0n, x)]), sb_last(i, x))