natPred_add_one — Mathlib

English

For any positive natural n, adding one to its predecessor gives back n: natPred(n) + 1 = n.

Русский

Для любого положительного натурального числа n, добавление единицы к его предшественнику возвращает n: natPred(n) + 1 = n.

LaTeX

$$$\forall n \in \mathbb{N}_+,\; \text{natPred}(n) + 1 = n$$$

Lean4

@[simp]
theorem natPred_add_one (n : ℕ+) : n.natPred + 1 = n :=
  (add_comm _ _).trans n.one_add_natPred

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