def pk.le0

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:101

import Base

101def pk.le0(+y: Nat) -> {Nat.is_le(0n, y) == True{} : Bool}:
102  match y:
103    case 0n:
104      {==}
105    case 1n+yp:
106      {==}