Reduce.fold_lt2_z: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as Reduce
Lines 121-126 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&start_line=121&end_line=126

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

# the hi = 0 case: the fold is lo
def fold_lt2_z(+t: Nat, +lo: Nat, +cv: Nat, +f: Nat, +ll: {Nat.is_lt(lo, t) == True{} : Bool}, +ef: {f == Nat.add(lo, Nat.mul(0n, cv)) : Nat}) -> {Nat.is_lt(f, t) == True{} : Bool}:
  %Equal.sym(Nat, f, Nat.add(lo, Nat.mul(0n, cv)), ef) : {Nat.is_lt(_, t) == True{} : Bool}
  %Equal.sym(Nat, Nat.mul(0n, cv), 0n, SR.zero_mul(cv)) : {Nat.is_lt(Nat.add(lo, _), t) == True{} : Bool}
  %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {Nat.is_lt(_, t) == True{} : Bool}
  ll

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_lt
  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/semiring.bend&name=zero_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero