no goals
F : Type ?u.53366
G : Type ?u.53369
α : Type u_1
M : Type ?u.53375
N : Type ?u.53378
inst✝ : DivisionMonoid α
a✝ b c : α
h : IsUnit b
a : α
⊢ a / b * b = a
rw [div_eq_mul_inv, h.inv_mul_cancel_right]