def wn.le0

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:47

import Base

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