Nat.cast_withBot

theorem Nat.cast_withBot : ∀ (n : ℕ), ↑n = ↑n

This theorem states that for any natural number `n`, the process of casting or converting `n` to another type and back to a natural number does not change the value of `n`. In other words, the cast operation is idempotent for natural numbers.

More concisely: For all natural numbers `n`, converting `n` to another type and then back to a natural number results in the original natural number `n`.