def wn.le0

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:49

import Base

49def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
50  match x:
51    case 0n:
52      {==}
53    case 1n+ +p:
54      {==}