def pred
import lawful-words@0.1.0.0/proof_nat.bend as ProofNatimport Base
126def pred(n: Nat) -> Nat:
127 match n:
128 case 0n:
129 0n
130 case 1n+p:
131 p
import lawful-words@0.1.0.0/proof_nat.bend as ProofNatimport Base
126def pred(n: Nat) -> Nat:
127 match n:
128 case 0n:
129 0n
130 case 1n+p:
131 p