no goals
F : Type ?u.57889
G : Type ?u.57892
α : Type u_1
M : Type ?u.57898
N : Type ?u.57901
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]