def off.le_zero

bend-osdev-bytes@0.1.1.0 · PROOF.bend:778

import Base

778def off.le_zero(+m: Nat) -> {Nat.is_le(0n, m) == True{} : Bool}:
779  match m:
780    case 0n:
781      {==}
782    case 1n+p:
783      {==}