a b : Int
H : b ≠ 0
this : (0 + a * b) / b = 0 / b + a
⊢ a * b / b = a
a b : Int
H : b ≠ 0
⊢ a * b / b = a
have := Int.add_mul_ediv_right 0 a H
no goals
a b : Int
H : b ≠ 0
this : (0 + a * b) / b = 0 / b + a
⊢ a * b / b = a
rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this