Documentation

Batteries.Data.Int.Order

@[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.