no goals
α : Type ?u.30697
β : Type ?u.30700
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -b / a = -(b / a)
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]