def aes_nat_predecessor

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:537

import Base

537def aes_nat_predecessor(n: Nat) -> Nat:
538    match n:
539        case 0n: 0n
540        case 1n+p: p