English
Let R be a type with a natural-number casting. For every n ≥ 2, the canonical embedding of n into R agrees with the numeral n, i.e. the cast of ofNat(n) equals ofNat(n).
Русский
Пусть R — множество с отображением натуральных чисел в R. Для любого n ≥ 2 отображение числа n в R через натуральное приведение совпадает с целочисленным представлением n: Nat.cast(ofNat(n)) = ofNat(n).
LaTeX
$$$\forall {R} [NatCast R] {n : \mathbb{N}} [Nat.AtLeastTwo n], (\mathrm{Nat.cast}(\mathrm{ofNat}(n)) : R) = \mathrm{ofNat}(n).$$$
Lean4
@[simp, norm_cast]
theorem cast_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : (Nat.cast ofNat(n) : R) = ofNat(n) :=
rfl
