def nz_of

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:415

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

415def nz_of(+k: Nat, +m: Nat, +h1: {C.fits(k, m) == False{} : Bool}) -> {Nat.is_eq(m, 0n) == False{} : Bool}:
416  match m:
417    case 0n:
418      NC.absurd_tf({Nat.is_eq(0n, 0n) == False{} : Bool}, Equal.trans(Bool, False{}, C.fits(k, 0n), True{}, Equal.sym(Bool, C.fits(k, 0n), False{}, h1), fz(k)))
419    case 1n+ +mp:
420      {==}