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

State before:
a b : ℤ
⊢ |a - b| % 2 = (a + b) % 2
Tactic:
rw [mod2_abs, Int.sub_eq_add_neg, Int.add_emod, Int.neg_emod_two, ←Int.add_emod]
State after:
no goals