def pk.lt0

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:108

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

import Base

108def pk.lt0(+x: Nat) -> {Nat.is_lt(x, 0n) == True{} : Bool} -> {False{} == True{} : Bool}:
109  match x:
110    case 0n:
111      h => h
112    case 1n+xp:
113      h => h

Uses (3)

Used by (1)

bend-osdev-pkcs7@0.1.0.0/PROOF:pk.lt_le