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