def nat.le_zero

bend-osdev-algo@0.1.0.0 · PROOF.bend:70

import Base

70def nat.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
71  match x:
72    case 0n:
73      {==}
74    case 1n+p:
75      {==}