Int.cast_neg_natCast

theorem Int.cast_neg_natCast : ∀ {R : Type u_2} [inst : DivisionRing R] (n : ℕ), ↑(-↑n) = -↑n

This theorem, `Int.cast_neg_natCast`, states that for any division ring `R` and any natural number `n`, casting the negation of the cast of `n` to `R` is equal to the negation of the cast of `n` to `R`. In other words, `-↑n = ↑-↑n` for all `n` in a division ring `R`. The restriction to `DivisionRing` is crucial to prevent instances where `R = ℤ`, which would lead to nontermination.

More concisely: In a division ring, the negation of the cast of a natural number is equal to the cast of the negation of that number. That is, `-↑n = ↑-↑n` for all natural numbers `n`.