succ_to_nat — Mathlib

English

For every PosNum n, the natural number corresponding to succ n equals n + 1.

Русский

Для любого PosNum n натуральная величина succ n равна n + 1.

LaTeX

$$$\\forall n:\\mathrm{PosNum}, (\\mathrm{succ}\,n : \\mathbb{N}) = n + 1$$$

Lean4

theorem succ_to_nat : ∀ n, (succ n : ℕ) = n + 1
  | 1 => rfl
  | bit0 _ => rfl
  | bit1 p =>
    (congr_arg (fun n ↦ n + n) (succ_to_nat p)).trans <| show ↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1 by simp [add_left_comm]

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