def nat.lt_zero

bend-osdev-bpf@0.1.0.0 · PROOF.bend:34

import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF

import Base

34def nat.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
35  match x:
36    case 0n:
37      {==}
38    case 1n+p:
39      {==}

Uses (3)

Used by (3)