def bq.le_zero

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:147

import Base

147def bq.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
148  match x:
149    case 0n:
150      {==}
151    case 1n+p:
152      {==}