Theorem: Int.mod'_eq (LeanCourse/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
a b : ℤ
⊢ mod' a b = a - b * div' a b
Tactic:
linarith [div'_add_mod' a b]
State after:
no goals