Theorem: Int.natAbs_le_iff (Util/Arithmetic.lean)

State before:
a b✝ c d : ℤ
b : ℕ
⊢ |a| ≤ b ↔ a ≤ ↑b ∧ -a ≤ ↑b
Tactic:
exact_mod_cast natAbs_le_iff' a b
State after:
no goals