no goals
F : Type ?u.57354
G : Type ?u.57357
α : Type u_1
M : Type ?u.57363
N : Type ?u.57366
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]