def posz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:15

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

15def posz(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_eq(n, 0n) == False{} : Bool}:
16  match n:
17    case 0n:
18      NC.absurd_tf({Nat.is_eq(0n, 0n) == False{} : Bool}, h)
19    case 1n+ +np:
20      {==}