Lits.ok16: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as Lits
Lines 28-33 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend&start_line=28&end_line=33

import Base

def ok16(+w: Nat, n: Nat, xs: List<&2, Nat>) -> Bool:
  match n xs:
    case 0n Nil{}: True{}
    case 0n x <> t: False{}
    case 1n+k Nil{}: False{}
    case 1n+k x <> t: Bool.and(Nat.is_lt(x, Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))), Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))))), ok16(w, k, t))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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.is_lt