Theorem: BrownCs22.Int.ModEq.refl (BrownCs22/Library/ModEq/Lemmas.lean)

State before:
n a : ℤ
⊢ a - a = n * 0
Tactic:
ring
State after:
no goals