Password.big: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as Password
Lines 94-97 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&start_line=94&end_line=97

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/logic.bend as L

def big(+tl: Nat, +q: Nat, +r: Nat, +e: {Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}, +ht: {Nat.is_le(65n, tl) == True{} : Bool}, +hq: {Nat.is_lt(q, 3n) == True{} : Bool}) -> Empty:
  +h1 = ge96(tl, ht)
  +h2 = L.subst(Nat, z => {Nat.is_lt(z, 96n) == True{} : Bool}, Nat.add(Nat.mul(q, 32n), r), Nat.add(tl, 31n), Equal.sym(Nat, Nat.add(tl, 31n), Nat.add(Nat.mul(q, 32n), r), e), lt96(q, r, hq, hr))
  L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(96n, 96n), False{}, Equal.sym(Bool, Nat.is_lt(96n, 96n), True{}, N.le_lt_trans(96n, Nat.add(tl, 31n), 96n, h1, h2)), N.lt_irrefl(96n)))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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_le
  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/argon2/password.bend&name=ge96
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=lt96
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=true_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_irrefl