elim — Mathlib

English

Let a, b ∈ ℤ with a < b, and P a proposition. If for every natural n the implication a + n.succ = b → P holds, then P holds.

Русский

Пусть a, b ∈ ℤ, a < b, и P — утверждение. Если для каждого натурального n верно: a + (n+1) = b → P, тогда P истинно.

LaTeX

$$$\forall a,b \in \mathbb{Z}, a < b \to \forall P, (\forall n \in \mathbb{N}, a + n.{\mathrm{succ}} = b \to P) \to P.$$$

Lean4

theorem elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(Nat.succ n) = b → P) : P :=
  Exists.elim (lt.dest h) h'

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