English
Induction principle on ℕ+: for any p : ℕ+ → Sort*, if p 1 and ∀ n, p n → p (n+1), then p a for all a ∈ ℕ+.
Русский
Индукционное правило на ℕ+: для любого p : ℕ+ → Sort*, если p(1) и ∀ n, p(n) → p(n+1), то p(a) для любого a ∈ ℕ+.
LaTeX
$$$\\\\forall p : \\\\mathbb{N}^+ \\\\to \\\\mathrm{Sort},\\\\ a \\\\in \\\\mathbb{N}^+,\\\\ p 1 \\\\to \\\\big( \\\\forall n, p n \\\\to p (n+1) \big) \\\\to \\\\ p a.$$$
Lean4
/-- An induction principle for `ℕ+`: it takes values in `Sort*`, so it applies also to Types,
not only to `Prop`. -/
@[elab_as_elim, induction_eliminator]
def recOn (n : ℕ+) {p : ℕ+ → Sort*} (one : p 1) (succ : ∀ n, p n → p (n + 1)) : p n :=
by
rcases n with ⟨n, h⟩
induction n with
| zero => exact absurd h (by decide)
| succ n IH =>
rcases n with - | n
· exact one
· exact succ _ (IH n.succ_pos)
