def internal_pred
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
134def internal_pred(n: Nat) -> Nat:
135 match n:
136 case 0n:
137 0n
138 case 1n+p:
139 p
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
134def internal_pred(n: Nat) -> Nat:
135 match n:
136 case 0n:
137 0n
138 case 1n+p:
139 p