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

State before:
a✝ b✝ c d a : ℤ
b : ℕ
⊢ a ≤ ↑b → -a ≤ ↑b → |a| ≤ b
Tactic:
exact_mod_cast @natAbs_le' a b
State after:
no goals