Theorem: Misc.Nat.eq_mul_of_div_eq_right (LeanSAT/Util/Misc.lean)

State before:
a b c : Nat
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c
Tactic:
rw [← H2, Nat.mul_div_cancel' H1]
State after:
no goals