def suffix_after

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/blist.bend:29

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/src/crypto/secp256k1/bytes.bend as B

29def suffix_after(n: Nat, bs: List<&2, U32>) -> {B.suffix(n, bs) == CV.after(n, bs) : List<&2, U32>}:
30  match n bs:
31    case 0n _:
32      {==}
33    case 1n+k Nil{}:
34      {==}
35    case 1n+k b <> t:
36      suffix_after(k, t)