def ckr.subn

bend-osdev-acpi@0.1.2.0 · PROOF_rsdp.bend:32

import Base

32def ckr.subn(+n: Nat) -> {Nat.sub(n, n) == 0n : Nat}:
33  match n:
34    case 0n:
35      {==}
36    case 1n+q:
37      ckr.subn(q)