Int.ofNat_natAbs_eq_of_nonneg

theorem Int.ofNat_natAbs_eq_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.natAbs = a

This theorem, `Int.ofNat_natAbs_eq_of_nonneg`, is an alias of `Int.natAbs_of_nonneg`. It states that for any integer `a`, if `a` is nonnegative (i.e., `a` is greater than or equal to 0), then the absolute value of `a` when converted to a natural number and then back to an integer is equal to `a` itself. This is an important property of nonnegative integers and their absolute values.

More concisely: For any integer `a` that is nonnegative, |a| (the absolute value of `a`) equals `a`.