def wn.not_lt_zero

bend-osdev-word64@0.1.1.0 · proof_value.bend:129

import Base

129def wn.not_lt_zero(x: Nat) -> {False{} == Nat.is_lt(x, 0n) : Bool}:
130  match x:
131    case 0n:
132      {==}
133    case 1n+p:
134      {==}