Top.hq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top
Lines 61-64 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&start_line=61&end_line=64

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I

# q = 4 sl
def hq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, Nat.div(Nat.div(I.blocks(m, p), p), 4n)) : Nat}:
  %Equal.sym(Nat, Nat.div(Nat.div(I.blocks(m, p), p), 4n), X(m, p), sl_eq(m, p, hp)) : {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, _) : Nat}
  q_eq(m, p, hp)

Uses (10):
  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.div
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=X
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=q_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend&name=sl_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=blocks