def Nat.pow
import Base811def Nat.pow(+a: Nat, b: Nat) -> Nat:
812 match b:
813 case 0n:
814 1n
815 case 1n+p:
816 Nat.mul(a, Nat.pow(a, p))
import Base811def Nat.pow(+a: Nat, b: Nat) -> Nat:
812 match b:
813 case 0n:
814 1n
815 case 1n+p:
816 Nat.mul(a, Nat.pow(a, p))