Uint64n.q_nz: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 60-61 of bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&start_line=60&end_line=61

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

def q_nz(+q: Nat, +s: Nat, +vn: Nat, +hn: {Nat.is_eq(vn, 0n) == False{} : Bool}, +e: {Nat.add(s, vn) == C.shift(64n, q) : Nat}) -> {Nat.is_eq(q, 0n) == False{} : Bool}:
  q_nz_c(q, s, vn, hn, e, Nat.is_eq(q, 0n), {==})

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=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=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&name=q_nz_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift