def ltz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqw.bend:8

import Base

8def ltz(+l: Nat) -> {Nat.is_lt(0n, l) == Bool.not(Nat.is_eq(l, 0n)) : Bool}:
9  match l:
10    case 0n:
11      {==}
12    case 1n+ +lp:
13      {==}