def wn.le_zero

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

import Base

122def wn.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
123  match x:
124    case 0n:
125      {==}
126    case 1n+p:
127      {==}