Listops.hz: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
Lines 179-185 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&start_line=179&end_line=185

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
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/ineq.bend as I

def hz(+lo: Nat, hi: Nat, +t: Nat, +hl: {Nat.is_lt(lo, t) == True{} : Bool}) -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}:
  match hi:
    case 0n:
      %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {True{} == Nat.is_lt(_, t) : Bool}
      Equal.sym(Bool, Nat.is_lt(lo, t), True{}, hl)
    case 1n+ +k:
      Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t), False{}, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t, N.le_trans(t, Nat.add(t, Nat.mul(k, t)), Nat.add(lo, Nat.add(t, Nat.mul(k, t))), N.le_add_right(t, Nat.mul(k, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(k, t))))))

Uses (12):
  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_eq
  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/ineq.bend&name=le_add_l
  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
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans