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

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