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

State before:
a b c d : ℤ
⊢ -↑(|a|) ≤ a
Tactic:
conv => rhs; rewrite [←a.neg_neg]
State after:
a b c d : ℤ
⊢ -↑(|a|) ≤ - -a

State before:
a b c d : ℤ
⊢ -↑(|a|) ≤ - -a
Tactic:
exact Int.neg_le_neg a.neg_le_natAbs
State after:
no goals