@[deprecated Int.natAbs_of_nonneg]

theorem Int.ofNat_natAbs_eq_of_nonneg {a : Int} (H : 0 ≤ a) : ↑a.natAbs = a

Alias of Int.natAbs_of_nonneg.