def posz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:59

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

59def posz(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_eq(n, 0n) == False{} : Bool}:
60  match n:
61    case 0n:
62      NC.absurd_tf({Nat.is_eq(0n, 0n) == False{} : Bool}, h)
63    case 1n+ +np:
64      {==}