Theorem: Usa1998P1.mod2_abs (Compfiles/Usa1998P1.lean)

State before:
a : ℤ
⊢ |a| % 2 = a % 2
Tactic:
cases' abs_cases a with h h <;> rw [h.1]
State after:
case inr
a : ℤ
h : |a| = -a ∧ a < 0
⊢ -a % 2 = a % 2

State before:
case inr
a : ℤ
h : |a| = -a ∧ a < 0
⊢ -a % 2 = a % 2
Tactic:
rw [Int.neg_emod_two]
State after:
no goals