~/jendhub

def nz_neg

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:335

import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

335# a negative word is nonzero
336def nz_neg(+w: Word(64n), +hn: {S.negative(w) == True{} : Bool}) -> {W.is_zero(64n, w) == False{} : Bool}:
337  nz_g(w, W.is_zero(64n, w), {==}, hn)

Uses (5)

Used by (1)