def zero_le

stelliferous@0.0.2.0 · proofs/nat_order.bend:126

import Base

126def zero_le(+a: Nat) -> {Nat.is_le(0n,a) == True{} : Bool}:
127  match a:
128    case 0n:
129      {==}
130    case 1n+p:
131      {==}