Theorem: Int.div'_add_mod' (LeanCourse/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
a b : ℤ
⊢ b * div' a b + mod' a b = a
Tactic:
rw [div', mod']
State after:
a b : ℤ
⊢ b * ((a + b / 2) / b) + ((a + b / 2) % b - b / 2) = a

State before:
a b : ℤ
⊢ b * ((a + b / 2) / b) + ((a + b / 2) % b - b / 2) = a
Tactic:
linarith [Int.ediv_add_emod (a + b / 2) b]
State after:
no goals