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

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