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

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