zneg_pred — Mathlib

English

For every ZNum n, the negation of its predecessor equals the successor of its negation: -n.pred = (-n).succ.

Русский

Для каждого ZNum n отрицание предшественника равно результату перехода к следующему после отрицания: -n.pred = (-n).succ.

LaTeX

$$$$-n.\text{pred} = (-n).\text{succ}.$$$$

Lean4

theorem zneg_pred (n : ZNum) : -n.pred = (-n).succ := by rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]

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