English
The predecessor function (partial) is Partrec.
Русский
Предшественник на натуральных числах (частично определяемый) — частично-рекурсивен.
LaTeX
$$$\text{Nat.Partrec }(\lambda n.\text{ppred } n)$$$
Lean4
theorem ppred : Partrec fun n => ppred n :=
have : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1 :=
(Primrec.ite (@PrimrecRel.comp _ _ _ _ _ _ _ _ _ Primrec.eq Primrec.fst (_root_.Primrec.succ.comp Primrec.snd))
(_root_.Primrec.const 0) (_root_.Primrec.const 1)).to₂
(of_primrec (Primrec₂.unpaired'.2 this)).rfind.of_eq fun n =>
by
cases n <;> simp
· exact eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by simp at h
· refine eq_some_iff.2 ?_
simp only [mem_rfind, decide_true, mem_some_iff, false_eq_decide_iff, true_and]
intro m h
simp [ne_of_gt h]
