a b : Int
H : mod a b = 0
this : mod a b + b * div a b = a
⊢ b * div a b = a
a b : Int
H : mod a b = 0
⊢ b * div a b = a
have := mod_add_div a b
no goals
a b : Int
H : mod a b = 0
this : mod a b + b * div a b = a
⊢ b * div a b = a
rwa [H, Int.zero_add] at this