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

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