def na.le_zero

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1694

import Base

1694def na.le_zero(a: Nat) -> {Nat.is_le(0n, a) == True{} : Bool}:
1695  match a:
1696    case 0n:
1697      {==}
1698    case 1n+q:
1699      {==}