def nat_lt_zero

bend-osdev-aead@0.1.0.0 · PROOF.bend:107

import Base

107def nat_lt_zero(x: Nat) -> {False{} == Nat.is_lt(x, 0n) : Bool}:
108  match x:
109    case 0n:
110      {==}
111    case 1n+p:
112      {==}