recOn_succ — Mathlib

English

recOn at n+1 is the successor of recOn at n: (n+1).recOn one succ = succ n (n.recOn one succ).

Русский

recOn на n+1 равен продолжению от recOn на n: (n+1).recOn one succ = succ n (n.recOn one succ).

LaTeX

$$$ (n+1).\\\\text{recOn}(one,succ) = \\\\text{succ } n ( n.\\\\text{recOn} (one,succ) ). $$$

Lean4

@[simp]
theorem recOn_succ (n : ℕ+) {p : ℕ+ → Sort*} (one succ) :
    @PNat.recOn (n + 1) p one succ = succ n (@PNat.recOn n p one succ) :=
  by
  obtain ⟨n, h⟩ := n
  cases n <;> [exact absurd h (by decide); rfl]

Похожие утверждения